idris 0.12.3 → 0.99

raw patch · 220 files changed

+4416/−3003 lines, 220 filesdep ~aesondep ~optparse-applicativedep ~safesetup-changedPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: aeson, optparse-applicative, safe

API changes (from Hackage documentation)

Files

• .travis.yml +3/−5
• CHANGELOG.md +22/−5
• CONTRIBUTORS +198/−39
• README.md +1/−0
• Setup.hs +1/−2
• codegen/idris-codegen-c/Main.hs +7/−5
• codegen/idris-codegen-javascript/Main.hs +4/−3
• codegen/idris-codegen-node/Main.hs +4/−5
• docs/conf.py +70/−9
• docs/effects/simpleeff.rst +4/−4
• docs/guides/type-providers-ffi.rst +2/−2
• docs/listing/idris-prompt-helloworld.txt +1/−1
• docs/listing/idris-prompt-interp.txt +1/−1
• docs/listing/idris-prompt-start.txt +1/−1
• docs/reference/compilation.rst +23/−15
• docs/reference/ffi.rst +1/−1
• docs/reference/uniqueness-types.rst +1/−1
• docs/tutorial/interfaces.rst +6/−6
• docs/tutorial/typesfuns.rst +2/−2
• docs/tutorial/views.rst +21/−0
• idris.cabal +8/−7
• libs/Makefile +0/−1
• libs/base/Data/HVect.idr +4/−4
• libs/base/Data/List/Views.idr +1/−1
• libs/base/Data/Vect.idr +98/−93
• libs/base/Makefile +3/−2
• libs/base/System/Concurrency/Channels.idr +9/−2
• libs/base/System/Concurrency/Raw.idr +6/−0
• libs/contrib/Data/Fin/Extra.idr +9/−0
• libs/contrib/Makefile +3/−2
• libs/contrib/contrib.ipkg +3/−1
• libs/effects/Makefile +1/−0
• libs/prelude/Builtins.idr +2/−1
• libs/prelude/Makefile +2/−1
• libs/prelude/Prelude.idr +14/−5
• libs/prelude/Prelude/Interactive.idr +10/−0
• libs/prelude/Prelude/Maybe.idr +9/−0
• libs/prelude/Prelude/Nat.idr +15/−0
• libs/prelude/Prelude/Show.idr +2/−2
• libs/prelude/Prelude/Strings.idr +2/−2
• libs/pruviloj/Makefile +1/−0
• libs/pruviloj/Pruviloj/Derive/Eliminators.idr +3/−3
• libs/pruviloj/Pruviloj/Internals.idr +3/−13
• libs/pruviloj/Pruviloj/Internals/TyConInfo.idr +1/−1
• main/Main.hs +21/−8
• man/idris.1 +13/−1
• mkpkg.sh +44/−6
• rts/idris_rts.c +18/−2
• rts/idris_rts.h +4/−0
• samples/effects/TreeTag.idr +2/−2
• samples/tutorial/classes.idr +1/−1
• src/IRTS/BCImp.hs +1/−1
• src/IRTS/Bytecode.hs +3/−2
• src/IRTS/CodegenC.hs +13/−13
• src/IRTS/CodegenCommon.hs +3/−3
• src/IRTS/CodegenJavaScript.hs +29/−32
• src/IRTS/Compiler.hs +28/−33
• src/IRTS/Defunctionalise.hs +5/−5
• src/IRTS/DumpBC.hs +2/−2
• src/IRTS/Exports.hs +1/−1
• src/IRTS/Inliner.hs +0/−1
• src/IRTS/JavaScript/AST.hs +2/−4
• src/IRTS/Lang.hs +5/−6
• src/IRTS/LangOpts.hs +6/−6
• src/IRTS/Portable.hs +3/−5
• src/IRTS/Simplified.hs +4/−4
• src/IRTS/System.hs +42/−21
• src/Idris/ASTUtils.hs +12/−8
• src/Idris/AbsSyntax.hs +63/−40
• src/Idris/AbsSyntaxTree.hs +64/−47
• src/Idris/Apropos.hs +5/−5
• src/Idris/CaseSplit.hs +15/−19
• src/Idris/Chaser.hs +8/−9
• src/Idris/CmdOptions.hs +23/−20
• src/Idris/Completion.hs +9/−11
• src/Idris/Core/Binary.hs +6/−5
• src/Idris/Core/CaseTree.hs +92/−34
• src/Idris/Core/Constraints.hs +3/−3
• src/Idris/Core/DeepSeq.hs +1/−1
• src/Idris/Core/Elaborate.hs +17/−13
• src/Idris/Core/Evaluate.hs +90/−84
• src/Idris/Core/Execute.hs +24/−22
• src/Idris/Core/ProofState.hs +24/−16
• src/Idris/Core/ProofTerm.hs +2/−2
• src/Idris/Core/TT.hs +46/−30
• src/Idris/Core/Typecheck.hs +9/−9
• src/Idris/Core/Unify.hs +2/−2
• src/Idris/Core/WHNF.hs +71/−26
• src/Idris/Coverage.hs +373/−919
• src/Idris/DSL.hs +2/−4
• src/Idris/DeepSeq.hs +8/−8
• src/Idris/Delaborate.hs +12/−12
• src/Idris/Directives.hs +2/−3
• src/Idris/Docs.hs +18/−8
• src/Idris/Docstrings.hs +7/−10
• src/Idris/Elab/AsPat.hs +1/−2
• src/Idris/Elab/Clause.hs +267/−89
• src/Idris/Elab/Data.hs +72/−30
• src/Idris/Elab/Implementation.hs +53/−34
• src/Idris/Elab/Interface.hs +54/−40
• src/Idris/Elab/Provider.hs +25/−29
• src/Idris/Elab/Quasiquote.hs +1/−1
• src/Idris/Elab/Record.hs +20/−24
• src/Idris/Elab/Rewrite.hs +4/−5
• src/Idris/Elab/RunElab.hs +5/−8
• src/Idris/Elab/Term.hs +83/−64
• src/Idris/Elab/Transform.hs +22/−26
• src/Idris/Elab/Type.hs +25/−30
• src/Idris/Elab/Utils.hs +38/−13
• src/Idris/Elab/Value.hs +23/−27
• src/Idris/ElabDecls.hs +32/−36
• src/Idris/Erasure.hs +25/−17
• src/Idris/Error.hs +10/−10
• src/Idris/IBC.hs +55/−39
• src/Idris/IdeMode.hs +9/−10
• src/Idris/IdrisDoc.hs +27/−34
• src/Idris/Imports.hs +5/−8
• src/Idris/Info.hs +21/−8
• src/Idris/Info/Show.hs +49/−1
• src/Idris/Inliner.hs +1/−1
• src/Idris/Interactive.hs +11/−12
• src/Idris/Main.hs +23/−28
• src/Idris/ModeCommon.hs +11/−14
• src/Idris/Output.hs +9/−12
• src/Idris/Package.hs +83/−77
• src/Idris/Package/Common.hs +1/−2
• src/Idris/Package/Parser.hs +11/−11
• src/Idris/Parser.hs +40/−45
• src/Idris/Parser/Data.hs +21/−27
• src/Idris/Parser/Expr.hs +6/−10
• src/Idris/Parser/Helpers.hs +20/−24
• src/Idris/Parser/Ops.hs +16/−19
• src/Idris/PartialEval.hs +85/−35
• src/Idris/Primitives.hs +5/−7
• src/Idris/ProofSearch.hs +7/−8
• src/Idris/Prover.hs +20/−26
• src/Idris/Providers.hs +3/−3
• src/Idris/REPL.hs +62/−72
• src/Idris/REPL/Browse.hs +6/−7
• src/Idris/REPL/Commands.hs +2/−2
• src/Idris/REPL/Parser.hs +38/−42
• src/Idris/Reflection.hs +20/−15
• src/Idris/Termination.hs +649/−0
• src/Idris/TypeSearch.hs +31/−28
• src/Idris/Unlit.hs +5/−3
• src/Idris/WhoCalls.hs +0/−2
• src/Util/DynamicLinker.hs +7/−7
• src/Util/Net.hs +2/−2
• src/Util/System.hs +7/−12
• stack-shell.nix +1/−1
• stack.yaml +2/−2
• test/TestData.hs +7/−3
• test/TestRun.hs +14/−11
• test/basic010/run +2/−2
• test/basic013/basic013.idr +35/−2
• test/basic013/expected +35/−1
• test/basic018/expected +1/−1
• test/delab001/run +1/−1
• test/docs001/run +1/−1
• test/docs002/run +1/−1
• test/docs003/run +1/−1
• test/docs004/run +1/−1
• test/docs005/run +1/−1
• test/docs006/docs006.idr +7/−0
• test/docs006/expected +16/−0
• test/docs006/input +1/−0
• test/docs006/run +3/−0
• test/dsl001/expected +7/−7
• test/dsl001/run +1/−1
• test/dsl001/test001.idr +0/−1
• test/ffi001/run +1/−1
• test/ffi002/run +1/−1
• test/ffi003/run +1/−1
• test/ffi004/run +1/−1
• test/idrisdoc009/run +1/−1
• test/interactive001/run +1/−1
• test/interactive002/run +1/−1
• test/interactive003/run +1/−1
• test/interactive004/run +1/−1
• test/interactive005/run +1/−1
• test/interactive006/run +1/−1
• test/interactive007/run +1/−1
• test/interactive008/run +1/−1
• test/interactive009/run +1/−1
• test/interactive010/run +1/−1
• test/interactive011/run +1/−1
• test/interactive012/run +1/−1
• test/interactive013/run +1/−1
• test/interfaces001/run +1/−1
• test/interfaces002/interfaces002.idr +2/−0
• test/layout001/run +1/−1
• test/primitives002/run +1/−1
• test/proof001/test029.idr +4/−5
• test/proof009/run +1/−1
• test/quasiquote006/run +1/−1
• test/reg041/run +1/−1
• test/reg075/run +1/−1
• test/reg076/expected +1/−0
• test/reg076/input +0/−0
• test/reg076/reg076.idr +11/−0
• test/reg076/run +4/−0
• test/regression001/coverage001.idr +79/−0
• test/regression001/eff001.idr +39/−0
• test/regression001/reg036.idr +2/−2
• test/regression001/run +5/−1
• test/regression002/expected +3/−3
• test/regression002/run +1/−1
• test/tactics001/Tactics.idr +4/−2
• test/totality011/expected +1/−1
• test/totality013/expected +2/−3
• test/totality015/totality015.idr +1/−1
• test/totality018/expected +1/−0
• test/totality018/run +3/−0
• test/totality018/totality018.idr +15/−0
• test/totality019/expected +2/−0
• test/totality019/run +4/−0
• test/totality019/totality019.idr +14/−0
• test/totality019/totality019a.idr +81/−0
• test/tutorial006/expected +5/−5
• test/unique004/run +1/−1

@@ -12,8 +12,6 @@       env: CABALVER="1.24" GHCVER="8.0.1" TESTS="test_c"       compiler: ": #GHC 8.0.1"     - env: CABALVER="1.20" GHCVER="7.6.3" TESTS="test_c"-      # separate caches for different compiler versions-      # until https://github.com/travis-ci/travis-ci/issues/4393 is resolved       compiler: ": #GHC 7.6.3"       addons: {apt: {packages: [cabal-install-1.20,ghc-7.6.3,cppcheck,hscolour], sources: [hvr-ghc]}}     - env: CABALVER="1.20" GHCVER="7.8.4" TESTS="test_c"@@ -58,9 +56,9 @@   - env   - if [[ $TRAVIS_OS_NAME == 'osx' ]];     then-        brew update; brew install ghc; brew install cabal-install;-        brew install libffi; brew install pkg-config; brew install cppcheck;-        brew install gnu-sed;+        brew update;+        brew outdated pkgconfig || brew install pkgconfig;+        brew install ghc cabal-install libffi cppcheck gnu-sed;         export PATH=$HOME/.cabal/bin:$PATH;         export SED=gsed;         export ZCAT=gzcat;

@@ -1,11 +1,11 @@-# New in 0.13:+# New in 0.99:  ## Language updates  * `record` syntax now allows updating fields, including nested fields,   by applying a function using the `$=` operator.  For example: -  ```+  ```idris   record Score where          constructor MkScore          correct : Nat@@ -21,6 +21,16 @@                         score->attempted $= (+1) } st   ``` +* Implicit parameter to interfaces are now allowed. For example:++  ```idris+  interface Shows (ts : Vect k Type) where+    shows : HVect ts -> Vect k String+  ```+  In this interface, `k` is an implicit parameter, but previously needed to+  be explicit++ ## Library updates  * The File Effect has been updated to take into account changes in@@ -40,18 +50,25 @@  * Idris' documentation system now displays the documentation for auto   implicits in the output of `:doc`. This is tested for in `docs005`.- * New command line flag `--info` that displays information about the installation.- * New command line flag `--sourcepath <dir>` that allows adding directories to the source search path.+* Allow 'installation' of a package's IdrisDoc documentation into a central location. The default location is the subdirectory `docs` of Idris' data directory.+  * New flag `--installdoc <ipkg>` provided to install documentation+  * New flag `--docdir` provided to show default documentation installation location.+  * New environment variable `IDRIS_DOC_PATH` to allow specification of an alternative installation path for documentation.+* Semantic meaning behind several environment variables has been clarified in documentation and code. See compilation section of the reference manual for more details.+* Interface parameter constraints are now printed in the output of `:doc`. This+  is tested for in `docs006`.+ ## Miscellaneous updates +* New, faster, better, implementation of the coverage checker * The test suite now uses [tasty-golden](https://hackage.haskell.org/package/tasty-golden). New tests must be registered in `test/TestData.hs`, as explained in the relevant `README.md`. * Added OSX and Windows continous integration with Travis and Appveyor.  ## UI Changes -* The :e command can now handle an $EDITOR with arguments in it, like "emacs -nw" +* The :e command can now handle an $EDITOR with arguments in it, like "emacs -nw"   # New in 0.12:

@@ -1,56 +1,215 @@ Thanks to the following for their help and contributions: -Ozgur Akgun+a3gis+Aaron Craelius+Adam Sandberg Eriksson+Adam Schønemann+Adolfo Ochagavía Ahmad Salim Al-Sibahi-Edward Chadwick Amsden-Michael R. Bernstein-Jan Bessai-Nicola Botta-Edwin Brady-Vitaly Bragilevsky-Jakob Brünker+Aistis Raulinaitis+Alex Feldman-Crough+Alexander Berntsen+Alexander Shabalin Alyssa Carter+Andreas Bogk+Andreas Reuleaux+Andrei Dziahel+Andrew Cann+Andrew Stewart Gibson+Andy Morris+Anthony Cantor+Anthony---faineance+Apostolis Xekoukoulotakis+Athan Clark+Bartosz Przygoda+Ben Gamari+Ben Sherman+ben-schulz+Benjamin Hodgson+Benjamin Saunders+Björn Aili+bmastenbrook+Brent Yorgey+Brian Koropoff+Brian McKenna+Bryn Keller+Calvin Beck+Carsten König Carter Charbonneau+Casper M. H. Holmgreen+cchantep+Cezar Ionescu+Chao-Hong Chen+Chetan Taralekar+Chris Allen+Christopher Schwaab+Cliff Harvey+Cliff L. Biffle+Colin Adams+comco+Craig McLaughlin+cswords+Daniel Waterworth+Daniël Heres+Darin Morrison+David Feuer+David Kraeutmann David Raymond Christiansen-Aaron Craelius-Jason Dagit-Adam Sandberg Eriksson-Guglielmo Fachini-Simon Fowler+defanor+Dennis Griffith+Dirk Ullrich+Dmitry Bushev+Dmitry Tsygankov+Dominic Mulligan+Dominik Peteler+Echo Nolan+Eduard Nicodei+Edward Amsden+Edward O'Callaghan+Edwin Brady+Eric Casteleijn+Eric Mertens+Eric Walkingshaw+Eric Weinstein+Erkin Batu Altunbaş+Ertugrul Söylemez+EvanR+Fabian Thorand+fiendfan1+Franklin Chen+Frederic Koehler+Friedrich von Never+Gabe McArthur+Gabor Greif+Gabriel Garcia+George Leontiev+Gleb Alexeyev Google-Zack Grannan-Sean Hunt-Cezar Ionescu+Greg Anderson+Greg Pfeil+Guglielmo Fachini+Hannes Mehnert Heath Johns+Heather+Hector A. Escobedo IV+identical snowflake+Ignas Vyšniauskas+Ilan Godik+Imuli Irene Knapp-Paul Koerbitz-Niklas Larsson-Shea Levy+Jack Henahan+Jacob Mitchell+Jakob Brünker+Jan Bessai+Jan de Muijnck-Hughes+Jan Doms+Jan Stolarek+Jason Dagit+Jason Gross+Jean-Remi Desjardins+Jeff Hemphill+Jefferson Carpenter+Jens Petersen+Jeremy W. Sherman+jhegedus42+joe9+Johannes Griebler+John Connor+John Dobronszki+John Wiegley+Jon Atack+Jonas Westerlund+Jonathan Sterling+Joseph Huang+Josh Vera+JP Smith+Juliusz Chroboczek+Jurriën Stutterheim+Jürgen Peters+Karlos Kaeeikaas+Kester Tong+lambdadomain+Langston Barrett+Leif Warner+Leon Schoorl+Luke Palmer+Mark Farrell+Markus Klink+Markus Pfeiffer Mathnerd314-Hannes Mehnert+Mattias Lundell+Matvey B. Aksenov+Matúš Tejiščák+Maxim Ivanov Mekeor Melire Melissa Mozifian-Jan de Muijnck-Hughes-Dominic Mulligan-Echo Nolan-Tom Prince-raichoo+Melvar Chen+Michael A. Smith+Michael Bernstein+Michael Gilliland+Michael Hensler+Michael Maloney+Michael McGirr+Michael Thompson+Michael Weiss+Miikka Koskinen+Mitchell Rosen+Miëtek Bak+Mort Yao+Nathan Dinsmore+Nicola Botta+Niklas Larsson+Norbert Melzer+Oskar Wickström+Ozgur Akgun+Patrik Jansson+Paul Koerbitz+Per Fredelius+Peter Minten Philip Rasmussen-Aistis Raulinaitis+PoroCYon+raichoo Reynir Reynisson+Ricky Elrod+Robert Clipsham+Robert Edström+Ross Meikleham+Ryan Scott+Sam Elliott+Sam T+Saurabh Rawat+Sean Hunt+Sebastian de Bellefon+Sebastian Dröge Seo Sanghyeon-Benjamin Saunders-Alexander Shabalin-Jeremy W. Sherman-Timo Petteri Sinnemäki-JP Smith+Sergei Trofimovich+Shane Pearman+Shea Levy+Simon Fowler startling-Chetan T-Matúš Tejiščák-Dirk Ullrich-Leif Warner-Daniel Waterworth-Eric Weinstein-Jonas Westerlund-Björn Aili+Stefan Bleibinhaus+stepcut+Stephen Drodge+Steven Shaw+Stuart Gale+suhorng+Sune Alkærsig+Sven Koschnicke+tdidriksen+Tenor Biel+Thomas Cooper+Tim Dysinger+Tim McGilchrist+Timo Petteri Sinnemäki+Tom Prince+TorosFanny+Trevor Elliott+uwap+Vitaly Bragilevsky+xged+XIE Yuheng+Yacine Hmito+Zack Grannan Zheng Jihui+zjhmale+Сухарик

@@ -6,6 +6,7 @@ [![Hackage](https://budueba.com/hackage/idris)](https://hackage.haskell.org/package/idris) [![Stackage LTS](http://stackage.org/package/idris/badge/lts)](http://stackage.org/lts/package/idris) [![Stackage Nightly](http://stackage.org/package/idris/badge/nightly)](http://stackage.org/nightly/package/idris)+[![IRC](https://img.shields.io/badge/IRC-%23idris-1e72ff.svg?style=flat)](https://www.irccloud.com/invite?channel=%23idris&hostname=irc.freenode.net&port=6697&ssl=1)  Idris (http://idris-lang.org/) is a general-purpose functional programming language with dependent types.

@@ -254,7 +254,7 @@       target = datadir $ L.absoluteInstallDirs pkg local copy        installStdLib = do-        let target' = target </> "libs"+        let target' = target -- </> "libs"         putStrLn $ "Installing libraries in " ++ target'         makeInstall "libs" target' @@ -267,7 +267,6 @@          let mandest = mandir (L.absoluteInstallDirs pkg local copy) ++ "/man1"          notice verbosity $ unwords ["Copying man page to", mandest]          installOrdinaryFiles verbosity mandest [("man", "idris.1")]-        makeInstall src target =          make verbosity [ "-C", src, "install" , "TARGET=" ++ target, "IDRIS=" ++ idrisCmd local]

@@ -1,19 +1,21 @@ module Main where -import Idris.Core.TT import Idris.AbsSyntax+import Idris.Core.TT import Idris.ElabDecls import Idris.Main-import IRTS.Compiler import IRTS.CodegenC+import IRTS.Compiler +import Util.System++import Paths_idris++import Control.Monad import System.Environment import System.Exit-import Control.Monad -import Paths_idris -import Util.System  data Opts = Opts { inputs :: [FilePath],                    interface :: Bool,

@@ -1,16 +1,17 @@ module Main where -import Idris.Core.TT import Idris.AbsSyntax+import Idris.Core.TT import Idris.ElabDecls import Idris.Main-import IRTS.Compiler import IRTS.CodegenJavaScript+import IRTS.Compiler +import Paths_idris+ import System.Environment import System.Exit -import Paths_idris  data Opts = Opts {                    inputs :: [FilePath]

@@ -1,17 +1,16 @@ module Main where -import Idris.Core.TT import Idris.AbsSyntax+import Idris.Core.TT import Idris.ElabDecls import Idris.Main--import IRTS.Compiler import IRTS.CodegenJavaScript+import IRTS.Compiler +import Paths_idris+ import System.Environment import System.Exit--import Paths_idris  data Opts = Opts { inputs :: [FilePath]                  , output :: FilePath

@@ -59,9 +59,9 @@ # built documents. # # The short X.Y version.-version = '0.12.3'+version = '0.99' # The full version, including alpha/beta/rc tags.-release = '0.12.3'+release = '0.99'  # The language for content autogenerated by Sphinx. Refer to documentation # for a list of supported languages.@@ -216,16 +216,76 @@  # -- Options for LaTeX output --------------------------------------------- +latex_title_page = r'''+\begin{titlepage}+    \vspace*{\fill}+    \begin{center}+        \includegraphics[width=0.25\textwidth]{idris-512x512.png}\par+        \vspace{1cm}+        {\huge\sffamily\bfseries Documentation for the Idris Language\par}+        \vspace{1cm}+        {\Large Version \version\par}+    \end{center}+    \vspace*{\fill}+\end{titlepage}+'''+ latex_elements = { # The paper size ('letterpaper' or 'a4paper'). 'papersize': 'a4paper', +'fontpkg': '',+'inputenc': '',+'utf8extra': '',+'releasename': 'Version',+ # The font size ('10pt', '11pt' or '12pt'). 'pointsize': '10pt',  # Additional stuff for the LaTeX preamble.-#'preamble': '',+'preamble': r'''+\usepackage{lmodern}+\usepackage[T1]{fontenc}+\usepackage[utf8x]{inputenc}+\usepackage{titlesec}+%+\usepackage{fancyhdr}+\fancypagestyle{plain}{%+  \renewcommand{\headrulewidth}{0pt}%+  \fancyhf{}%+  \fancyfoot[C]{\textsf{\thepage}}+}+\pagestyle{fancy}+\fancyhf{}+\fancyhead[LE,RO]{\textsf{\bfseries{v\version}}}+\fancyhead[LO,RE]{\textsf{\bfseries\leftmark}}+%\fancyhead[LO]{\textsf{\bfseries{\leftmark}}}+%\fancyhead[RO]{\textsf{\bfseries{v\version}}}+%\fancyhead[RE]{\textsf{\bfseries{\leftmark}}}+%\fancyhead[LE]{\textsf{\bfseries{v\version}}}+\fancyfoot[C]{\textsf{\thepage}}+\renewcommand{\footrulewidth}{0pt}+\renewcommand{\headrulewidth}{0pt}+%+\usepackage[font={small,it}]{caption}+\titleformat{\section}+  {\normalfont\sffamily\Large\bfseries\color{black}}+  {\thesection}{1em}{}+\titleformat{\subsection}+  {\sffamily\large\bfseries\color{black}}+  {\thesubsection}{1em}{}+\titleformat{\subsubsection}+  {\sffamily\normalsize\bfseries\color{black}}+  {\thesubsubsection}{1em}{}+\titleformat{\paragraph}{\normalfont\normalsize\slshape}{\theparagraph}{1em}{}+\setlength{\parskip}{1em}+%+\hypersetup{colorlinks = false}+\definecolor{VerbatimBorderColor}{rgb}{1,1,1}+''', +'maketitle': latex_title_page+ # Latex figure (float) alignment #'figure_align': 'htbp', }@@ -234,15 +294,16 @@ # (source start file, target name, title, #  author, documentclass [howto, manual, or own class]). latex_documents = [-  ('tutorial/index',  'idris-tutorial.tex',  u'The Idris Tutorial',    u'The Idris Community', 'manual'),-  ('guides/index',    'idris-guides.tex',    u'Idris Tutorial Series', u'The Idris Community', 'manual'),-#  ('reference/index', 'idris-reference.tex', u'The Idris Reference',   u'The Idris Community', 'manual'),-    ('effects/index',  'eff-tutorial.tex',  u'The Effects Tutorial',    u'The Idris Community', 'manual')-    ]+  ('index',  'idris.tex',  u'Documentation for the Idris Language',    u'The Idris Community', 'report')+] ++latex_show_pagerefs = True+latex_show_url = 'footnote'+ # The name of an image file (relative to this directory) to place at the top of # the title page.-#latex_logo = None+latex_logo = '../icons/idris-512x512.png'  # For "manual" documents, if this is true, then toplevel headings are parts, # not chapters.

@@ -495,8 +495,8 @@     Env = List (String, Integer)      eval : Expr -> Eff Integer [EXCEPTION String, STATE Env]-    eval (Val x) = return x-    eval (Add l r) = return $ !(eval l) + !(eval r)+    eval (Val x)   = pure x+    eval (Add l r) = pure $ !(eval l) + !(eval r)  Note that we are using ``!``-notation to avoid having to bind subexpressions in a ``do`` block. Next, we add a case for evaluating@@ -506,7 +506,7 @@      eval (Var x) = case lookup x !get of                         Nothing => raise $ "No such variable " ++ x-                        Just val => return val+                        Just val => pure val  This retrieves the state (with ``get``, supported by the ``STATE Env`` effect) and raises an exception if the variable is not in the@@ -559,7 +559,7 @@      eval (Random upper) = do val <- rndInt 0 upper                              putStrLn (show val)-                             return val+                             pure val  If we try this without extending the effects list, we would see an error something like the following:

@@ -53,8 +53,8 @@       putStrLn "I'm sorry, I don't know how big size_t is. Can you tell me, in bytes?"       resp <- getLine       case readInt resp of-         Just sizeTSize => return (Provide sizeTSize)-         Nothing => return (Error "I'm sorry, I don't understand.")+         Just sizeTSize => pure (Provide sizeTSize)+         Nothing => pure (Error "I'm sorry, I don't understand.")     -- the readInt function is left as an exercise  We assume that whoever's compiling the library knows the size of

@@ -1,7 +1,7 @@ $ idris hello.idr      ____    __     _     /  _/___/ /____(_)____-    / // __  / ___/ / ___/     Version 0.12.3+    / // __  / ___/ / ___/     Version 0.99   _/ // /_/ / /  / (__  )      http://www.idris-lang.org/  /___/\__,_/_/  /_/____/       Type :? for help 

@@ -1,7 +1,7 @@ $ idris interp.idr      ____    __     _     /  _/___/ /____(_)____-    / // __  / ___/ / ___/     Version 0.12.3+    / // __  / ___/ / ___/     Version 0.99   _/ // /_/ / /  / (__  )      http://www.idris-lang.org/  /___/\__,_/_/  /_/____/       Type :? for help 

@@ -1,7 +1,7 @@ $ idris     ____    __     _    /  _/___/ /____(_)____-   / // __  / ___/ / ___/     Version 0.12.3+   / // __  / ___/ / ___/     Version 0.99  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/ /___/\__,_/_/  /_/____/       Type :? for help 

@@ -86,22 +86,30 @@  * `IDRIS_CC` Change the `C` compiler used by the `C` backend. * `IDRIS_CFLAGS` Change the `C` flags passed to the `C` compiler.-* `TARGET`   Change the target directory to generate files.-* `IDRIS_LIBRARY_PATH` Change the location of where installed packages are found.+* `TARGET`   Change the target directory i.e. `data dir` where Idris installs files when installing using Cabal/Stack.+* `IDRIS_LIBRARY_PATH` Change the location of where installed packages are found/installed.+* `IDRIS_DOC_PATH`  Change the location of where generated idrisdoc for packages are installed. -Alternativly, and perhaps a cleaner approach is to configure these-options using the CLI options.  Idris also supports options to augment-the paths used, and pass options to the code generator backend.+.. note:: -The option `--cg-opt <ARG>` can be used to pass options to the code-generator. The format of `<ARG>` is dependent on the selected backend.+   In versions of Idris prior to 0.12.3 the environment variables+   `IDRIS_LIBRARY_PATH` and `TARGET` were both used to affect the+   installation of single packages and direct where Idris installed+   its data. The meaning of these variables has changed, and command+   line options are preferred when changing where individual packages+   are installed. -Further, Idris does support multiple include paths.  The CLI option-`-i <dir>` allows you to add a directory to the library search path; this-option can be used multiple times. This is a cleaner option when you-wish to add single directories to the `IDRIS_LIBRARY_PATH` than-ammending `IDRIS_LIBRARY_PATH` directly.-To add directories to the source search path, use the `--sourcepath <dir>` option.+The CLI option `--ibcsubdir` can be used to direct where generated IBC+files are placed.  However, this means Idris will install files in a+non-standard location separate from the rest of the installed+packages. The CLI option `--idrispath <dir>` allows you to add a+directory to the library search path; this option can be used multiple+times and can be shortened to `-i <dir>`. Similary, the `--sourcepath+<dir>` option can be used to add directories to the source search+path. There is no shortened version for this option as `-s` is a+reserved flag. -Moreover, rather than using `TARGET` the CLI option `--ibcsubdir` can-be used to direct where built IBC files are placed.+Further, Idris also supports options to augment the paths used, and+pass options to the code generator backend.  The option `--cg-opt+<ARG>` can be used to pass options to the code generator. The format+of `<ARG>` is dependent on the selected backend.

@@ -361,4 +361,4 @@       timeout <- jscall "setTimeout(%0, %1)"                         (JsFn (() -> JS_IO ()) -> Int -> JS_IO Ptr)                         (MkJsFn f) millis-      return $ MkTimeout timeout+      pure $ MkTimeout timeout

@@ -212,7 +212,7 @@     foo xs = do let f = \x : Int => showU xs                 putStrLn $ free xs                 putStrLn $ f 42-                return ()+                pure ()  Since ``lend`` is implicit, in practice for functions to lend and borrow values merely requires the argument to be marked as ``Borrowed``. We can

@@ -232,7 +232,7 @@     m_add : Maybe Int -> Maybe Int -> Maybe Int     m_add x y = do x' <- x -- Extract value from x                    y' <- y -- Extract value from y-                   return (x' + y') -- Add them+                   pure (x' + y') -- Add them  This function will extract the values from ``x`` and ``y``, if they are both available, or return ``Nothing`` if one or both are not ("fail fast"). Managing the@@ -270,7 +270,7 @@ .. code-block:: idris      readNumbers : IO (Maybe (Nat, Nat))-    readNumbers = +    readNumbers =       do x <- readNumber          case x of               Nothing => pure Nothing@@ -286,7 +286,7 @@ .. code-block:: idris      readNumbers : IO (Maybe (Nat, Nat))-    readNumbers = +    readNumbers =       do Just x_ok <- readNumber          Just y_ok <- readNumber          pure (Just (x_ok, y_ok))@@ -298,7 +298,7 @@ .. code-block:: idris      readNumbers : IO (Maybe (Nat, Nat))-    readNumbers = +    readNumbers =       do Just x_ok <- readNumber | Nothing => pure Nothing          Just y_ok <- readNumber | Nothing => pure Nothing          pure (Just (x_ok, y_ok))@@ -321,7 +321,7 @@ .. code-block:: idris      m_add : Maybe Int -> Maybe Int -> Maybe Int-    m_add x y = return (!x + !y)+    m_add x y = pure (!x + !y)  The notation ``!expr`` means that the expression ``expr`` should be evaluated and then implicitly bound. Conceptually, we can think of@@ -388,7 +388,7 @@  .. code-block:: idris -    do { qual1; qual2; ...; qualn; return exp; }+    do { qual1; qual2; ...; qualn; pure exp; }  Using monad comprehensions, an alternative definition for ``m_add`` would be:

@@ -635,12 +635,12 @@ type ``IO a``, and puts the result, of type ``a`` into the variable ``x``. In this case, ``getLine`` returns an ``IO String``, so ``name`` has type ``String``. Indentation is significant — each statement in-the do block must begin in the same column. The ``return`` operation+the do block must begin in the same column. The ``pure`` operation allows us to inject a value directly into an IO operation:  .. code-block:: idris -    return : a -> IO a+    pure : a -> IO a  As we will see later, ``do`` notation is more general than this, and can be overloaded.

@@ -92,6 +92,27 @@ We will return to this function in Section :ref:`sect-provisional` to complete the definition of ``parity``. +With and proofs+===============+To use a dependent pattern match for theorem proving, it is sometimes necessary+to explicitly construct the proof resulting from the pattern match.+To do this, you can postfix the with clause with ``proof p`` and the proof+generated by the pattern match will be in scope and named ``p``. For example:++.. code-block:: idris++    data Foo = FInt Int | FBool Bool++    optional : Foo -> Maybe Int+    optional (FInt x) = Just x+    optional (FBool b) = Nothing++    isFInt : (foo:Foo) -> Maybe (x : Int ** (optional foo = Just x))+    isFInt foo with (optional foo) proof p+      isFInt foo | Nothing = Nothing           -- here, p : Nothing = optional foo+      isFInt foo | (Just x) = Just (x ** Refl) -- here, p : Just x = optional foo++ .. [1] Conor McBride and James McKinna. 2004. The view from the        left. J. Funct. Program. 14, 1 (January 2004),        69-111. DOI=10.1017/S0956796803004829

@@ -1,5 +1,5 @@ Name:           idris-Version:        0.12.3+Version:        0.99 License:        BSD3 License-file:   LICENSE Author:         Edwin Brady@@ -40,7 +40,7 @@                 .                 * Hugs style interactive environment -Cabal-Version:  >= 1.8+Cabal-Version:  >= 1.8.1  Build-type:     Custom @@ -209,6 +209,7 @@                 , Idris.REPL                 , Idris.REPL.Parser                 , Idris.REPL.Commands+                , Idris.Termination                 , Idris.Transforms                 , Idris.TypeSearch                 , Idris.Unlit@@ -251,7 +252,7 @@                 , Tools_idris    Build-depends:  base >=4 && <5-                , aeson >= 0.6 && < 0.12+                , aeson >= 0.6 && < 1.1                 , annotated-wl-pprint >= 0.7 && < 0.8                 , ansi-terminal < 0.7                 , ansi-wl-pprint < 0.7@@ -271,7 +272,7 @@                 , ieee754 >= 0.7 && < 0.8                 , mtl >= 2.1 && < 2.3                 , network < 2.7-                , optparse-applicative >= 0.11 && < 0.13+                , optparse-applicative >= 0.11 && < 0.14                 , parsers >= 0.9 && < 0.13                 , pretty < 1.2                 , regex-tdfa >= 1.2@@ -288,7 +289,7 @@                 , vector < 0.12                 , vector-binary-instances < 0.3                 , zip-archive > 0.2.3.5 && < 0.4-                , safe+                , safe == 0.3.9                 , fsnotify >= 0.2 && < 2.2                 , async < 2.2 @@ -362,7 +363,7 @@                , filepath                , directory                , haskeline >= 0.7-               , optparse-applicative >= 0.11 && < 0.13+               , optparse-applicative >= 0.11 && < 0.14                , tagged                , tasty >= 0.8                , tasty-golden >= 2.0@@ -374,7 +375,7 @@     ghc-prof-options: -auto-all -caf-all-  ghc-options:      -threaded -rtsopts -funbox-strict-fields+  ghc-options:      -threaded -rtsopts -with-rtsopts=-N -funbox-strict-fields  Executable idris-codegen-c   Main-is:        Main.hs

@@ -34,5 +34,4 @@ 	$(MAKE)	-C effects doc_clean 	$(MAKE)	-C pruviloj doc_clean - .PHONY: build install clean doc doc_clean

@@ -59,16 +59,16 @@       decEq (z::xs) (z::ys) | Yes Refl | No ctr = No (ctr . hvectInjective2)     decEq (x::xs) (y::ys) | No ctr = No (ctr . hvectInjective1) -interface Shows (k : Nat) (ts : Vect k Type) where+interface Shows (ts : Vect k Type) where   shows : HVect ts -> Vect k String -implementation Shows Z [] where+implementation Shows [] where   shows [] = [] -implementation (Show t, Shows k ts) => Shows (S k) (t::ts) where+implementation (Show t, Shows ts) => Shows (t::ts) where   shows (x::xs) = show x :: shows xs -implementation (Shows k ts) => Show (HVect ts) where+implementation (Shows ts) => Show (HVect ts) where   show xs = "[" ++ (pack . intercalate [','] . map unpack . toList $ shows xs) ++ "]"  ||| Extract an arbitrary element of the correct type.

@@ -187,7 +187,7 @@ data VList : List a -> Type where      VNil : VList []      VOne : VList [x]-     VCons : {x : a} -> {y : a} -> {xs : List a} -> +     VCons : {x : a} -> {y : a} -> .{xs : List a} ->               (rec : VList xs) -> VList (x :: xs ++ [y])  total

@@ -9,13 +9,15 @@ infixr 7 ::  ||| Vectors: Generic lists with explicit length in the type+||| @ len the length of the list+||| @ elem the type of elements %elim-data Vect : Nat -> Type -> Type where+data Vect : (len : Nat) -> (elem : Type) -> Type where   ||| Empty vector-  Nil  : Vect Z a-  ||| A non-empty vector of length `S k`, consisting of a head element and-  ||| the rest of the list, of length `k`.-  (::) : (x : a) -> (xs : Vect k a) -> Vect (S k) a+  Nil  : Vect Z elem+  ||| A non-empty vector of length `S len`, consisting of a head element and+  ||| the rest of the list, of length `len`.+  (::) : (x : elem) -> (xs : Vect len elem) -> Vect (S len) elem  -- Hints for interactive editing %name Vect xs,ys,zs,ws@@ -28,14 +30,14 @@ ||| ||| **Note**: this is only useful if you don't already statically know the length ||| and you want to avoid matching the implicit argument for erasure reasons.-||| @ n the length (provably equal to the return value)+||| @ len the length (provably equal to the return value) ||| @ xs the vector-length : (xs : Vect n a) -> Nat+length : (xs : Vect len elem) -> Nat length [] = 0 length (x::xs) = 1 + length xs  ||| Show that the length function on vectors in fact calculates the length-private lengthCorrect : (n : Nat) -> (xs : Vect n a) -> length xs = n+private lengthCorrect : (len : Nat) -> (xs : Vect len elem) -> length xs = len lengthCorrect Z     []        = Refl lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in Refl @@ -44,44 +46,44 @@ --------------------------------------------------------------------------------  ||| All but the first element of the vector-tail : Vect (S n) a -> Vect n a+tail : Vect (S len) elem -> Vect len elem tail (x::xs) = xs  ||| Only the first element of the vector-head : Vect (S n) a -> a+head : Vect (S len) elem -> elem head (x::xs) = x  ||| The last element of the vector-last : Vect (S n) a -> a+last : Vect (S len) elem -> elem last (x::[])    = x last (x::y::ys) = last $ y::ys  ||| All but the last element of the vector-init : Vect (S n) a -> Vect n a+init : Vect (S len) elem -> Vect len elem init (x::[])    = [] init (x::y::ys) = x :: init (y::ys)  ||| Extract a particular element from a vector-index : Fin n -> Vect n a -> a+index : Fin len -> Vect len elem -> elem index FZ     (x::xs) = x index (FS k) (x::xs) = index k xs   ||| Insert an element at a particular index-insertAt : Fin (S n) -> a -> Vect n a -> Vect (S n) a+insertAt : Fin (S len) -> elem -> Vect len elem -> Vect (S len) elem insertAt FZ     y xs      = y :: xs insertAt (FS k) y (x::xs) = x :: insertAt k y xs insertAt (FS k) y []      = absurd k  ||| Construct a new vector consisting of all but the indicated element-deleteAt : Fin (S n) -> Vect (S n) a -> Vect n a-deleteAt           FZ     (x::xs) = xs-deleteAt {n = S m} (FS k) (x::xs) = x :: deleteAt k xs-deleteAt {n = Z}   (FS k) (x::xs) = absurd k-deleteAt           _      []      impossible+deleteAt : Fin (S len) -> Vect (S len) elem -> Vect len elem+deleteAt             FZ     (x::xs) = xs+deleteAt {len = S m} (FS k) (x::xs) = x :: deleteAt k xs+deleteAt {len = Z}   (FS k) (x::xs) = absurd k+deleteAt             _      []      impossible  ||| Replace an element at a particlar index with another-replaceAt : Fin n -> t -> Vect n t -> Vect n t+replaceAt : Fin len -> elem -> Vect len elem -> Vect len elem replaceAt FZ     y (x::xs) = y :: xs replaceAt (FS k) y (x::xs) = x :: replaceAt k y xs @@ -89,7 +91,7 @@ ||| @ i the index to replace at ||| @ f the update function ||| @ xs the vector to replace in-updateAt : (i : Fin n) -> (f : t -> t) -> (xs : Vect n t) -> Vect n t+updateAt : (i : Fin len) -> (f : elem -> elem) -> (xs : Vect len elem) -> Vect len elem updateAt FZ     f (x::xs) = f x :: xs updateAt (FS k) f (x::xs) = x :: updateAt k f xs @@ -99,13 +101,13 @@  ||| Get the first n elements of a Vect ||| @ n the number of elements to take-take : (n : Nat) -> Vect (n + m) a -> Vect n a+take : (n : Nat) -> Vect (n + m) elem -> Vect n elem take Z     xs        = [] take (S k) (x :: xs) = x :: take k xs  ||| Remove the first n elements of a Vect ||| @ n the number of elements to remove-drop : (n : Nat) -> Vect (n + m) a -> Vect m a+drop : (n : Nat) -> Vect (n + m) elem -> Vect m elem drop Z     xs        = xs drop (S k) (x :: xs) = drop k xs @@ -113,7 +115,7 @@ ||| Boolean predicate. ||| ||| @ p the predicate-takeWhile : (p : a -> Bool) -> Vect n a -> (q ** Vect q a)+takeWhile : (p : elem -> Bool) -> Vect len elem -> (q ** Vect q elem) takeWhile p []      = (_ ** []) takeWhile p (x::xs) =   let (len ** ys) = takeWhile p xs@@ -126,7 +128,7 @@ ||| Boolean predicate. ||| ||| @ p the predicate-dropWhile : (p : a -> Bool) -> Vect n a -> (q ** Vect q a)+dropWhile : (p : elem -> Bool) -> Vect len elem -> (q ** Vect q elem) dropWhile p [] = (_ ** []) dropWhile p (x::xs) =   if p x then@@ -139,9 +141,9 @@ --------------------------------------------------------------------------------  ||| Reverse the order of the elements of a vector-reverse : Vect n a -> Vect n a+reverse : Vect len elem -> Vect len elem reverse xs = go [] xs-  where go : Vect n a -> Vect m a -> Vect (n+m) a+  where go : Vect n elem -> Vect m elem -> Vect (n+m) elem         go {n}         acc []        = rewrite plusZeroRightNeutral n in acc         go {n} {m=S m} acc (x :: xs) = rewrite sym $ plusSuccRightSucc n m                                        in go (x::acc) xs@@ -149,11 +151,11 @@ ||| Alternate an element between the other elements of a vector ||| @ sep the element to intersperse ||| @ xs the vector to separate with `sep`-intersperse : (sep : a) -> (xs : Vect n a) -> Vect (n + pred n) a+intersperse : (sep : elem) -> (xs : Vect len elem) -> Vect (len + pred len) elem intersperse sep []      = [] intersperse sep (x::xs) = x :: intersperse' sep xs   where-    intersperse' : a -> Vect n a -> Vect (n + n) a+    intersperse' : elem -> Vect n elem -> Vect (n + n) elem     intersperse'         sep []      = []     intersperse' {n=S n} sep (x::xs) = rewrite sym $ plusSuccRightSucc n n                                        in sep :: x :: intersperse' sep xs@@ -163,17 +165,17 @@ --------------------------------------------------------------------------------  -fromList' : Vect n a -> (l : List a) -> Vect (length l + n) a+fromList' : Vect len elem -> (l : List elem) -> Vect (length l + len) elem fromList' ys [] = ys-fromList' {n} ys (x::xs) =-  rewrite (plusSuccRightSucc (length xs) n) ==>-          Vect (plus (length xs) (S n)) a in+fromList' {len} ys (x::xs) =+  rewrite (plusSuccRightSucc (length xs) len) ==>+          Vect (plus (length xs) (S len)) elem in   fromList' (x::ys) xs  ||| Convert a list to a vector. ||| ||| The length of the list should be statically known.-fromList : (l : List a) -> Vect (length l) a+fromList : (l : List elem) -> Vect (length l) elem fromList l =   rewrite (sym $ plusZeroRightNeutral (length l)) in   reverse $ fromList' [] l@@ -183,30 +185,31 @@ --------------------------------------------------------------------------------  ||| Append two vectors-(++) : Vect m a -> Vect n a -> Vect (m + n) a+(++) : (xs : Vect m elem) -> (ys : Vect n elem) -> Vect (m + n) elem (++) []      ys = ys (++) (x::xs) ys = x :: xs ++ ys -||| Repeate some value n times-||| @ n the number of times to repeat it+||| Repeate some value some number of times.+|||+||| @ len the number of times to repeat it ||| @ x the value to repeat-replicate : (n : Nat) -> (x : a) -> Vect n a+replicate : (len : Nat) -> (x : elem) -> Vect len elem replicate Z     x = [] replicate (S k) x = x :: replicate k x  ||| Merge two ordered vectors-mergeBy : (a -> a -> Ordering) -> Vect n a -> Vect m a -> Vect (n + m) a+mergeBy : (elem -> elem -> Ordering) -> (xs : Vect n elem) -> (ys : Vect m elem) -> Vect (n + m) elem mergeBy order [] [] = [] mergeBy order [] (x :: xs) = x :: xs-mergeBy {n = S k} order (x :: xs) [] = rewrite plusZeroRightNeutral (S k) in  +mergeBy {n = S k} order (x :: xs) [] = rewrite plusZeroRightNeutral (S k) in                                                x :: xs-mergeBy {n = S k} {m = S k'} order (x :: xs) (y :: ys) +mergeBy {n = S k} {m = S k'} order (x :: xs) (y :: ys)      = case order x y of             LT => x :: mergeBy order xs (y :: ys)-            _  => rewrite sym (plusSuccRightSucc k k') in +            _  => rewrite sym (plusSuccRightSucc k k') in                              y :: mergeBy order (x :: xs) ys -merge : Ord a => Vect n a -> Vect m a -> Vect (n + m) a+merge : Ord elem => Vect n elem -> Vect m elem -> Vect (n + m) elem merge = mergeBy compare  --------------------------------------------------------------------------------@@ -223,26 +226,26 @@ zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys  ||| Combine three equal-length vectors into a vector with some function-zipWith3 : (a -> b -> c -> d) -> Vect n a -> Vect n b -> Vect n c -> Vect n d+zipWith3 : (a -> b -> c -> d) -> (xs : Vect n a) -> (ys : Vect n b) -> (zs : Vect n c) -> Vect n d zipWith3 f []      []      []      = [] zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs  ||| Combine two equal-length vectors pairwise-zip : Vect n a -> Vect n b -> Vect n (a, b)+zip : (xs : Vect n a) -> (ys : Vect n b) -> Vect n (a, b) zip = zipWith (\x,y => (x,y))  ||| Combine three equal-length vectors elementwise into a vector of tuples-zip3 : Vect n a -> Vect n b -> Vect n c -> Vect n (a, b, c)+zip3 : (xs : Vect n a) -> (ys : Vect n b) -> (zs : Vect n c) -> Vect n (a, b, c) zip3 = zipWith3 (\x,y,z => (x,y,z))  ||| Convert a vector of pairs to a pair of vectors-unzip : Vect n (a, b) -> (Vect n a, Vect n b)+unzip : (xs : Vect n (a, b)) -> (Vect n a, Vect n b) unzip []           = ([], []) unzip ((l, r)::xs) with (unzip xs)   | (lefts, rights) = (l::lefts, r::rights)  ||| Convert a vector of three-tuples to a triplet of vectors-unzip3 : Vect n (a, b, c) -> (Vect n a, Vect n b, Vect n c)+unzip3 : (xs : Vect n (a, b, c)) -> (Vect n a, Vect n b, Vect n c) unzip3 []            = ([], [], []) unzip3 ((l,c,r)::xs) with (unzip3 xs)   | (lefts, centers, rights) = (l::lefts, c::centers, r::rights)@@ -251,7 +254,7 @@ -- Equality -------------------------------------------------------------------------------- -implementation (Eq a) => Eq (Vect n a) where+implementation (Eq elem) => Eq (Vect len elem) where   (==) []      []      = True   (==) (x::xs) (y::ys) = x == y && xs == ys @@ -260,7 +263,7 @@ -- Order -------------------------------------------------------------------------------- -implementation Ord a => Ord (Vect n a) where+implementation Ord elem => Ord (Vect len elem) where   compare []      []      = EQ   compare (x::xs) (y::ys) = compare x y `thenCompare` compare xs ys @@ -283,7 +286,7 @@ ||| ||| @ f the partial function (expressed by returning `Maybe`) ||| @ xs the vector to check for results-mapMaybe : (f : a -> Maybe b) -> (xs : Vect n a) -> (m : Nat ** Vect m b)+mapMaybe : (f : a -> Maybe b) -> (xs : Vect len a) -> (m : Nat ** Vect m b) mapMaybe f []      = (_ ** []) mapMaybe f (x::xs) =   let (len ** ys) = mapMaybe f xs@@ -308,7 +311,7 @@ --------------------------------------------------------------------------------  ||| Flatten a vector of equal-length vectors-concat : Vect m (Vect n a) -> Vect (m * n) a+concat : (xss : Vect m (Vect n elem)) -> Vect (m * n) elem concat []      = [] concat (v::vs) = v ++ concat vs @@ -323,7 +326,7 @@ -- Scans -------------------------------------------------------------------------------- -scanl : (b -> a -> b) -> b -> Vect n a -> Vect (S n) b+scanl : (res -> elem -> res) -> res -> Vect len elem -> Vect (S len) res scanl f q []      = [q] scanl f q (x::xs) = q :: scanl f (f q x) xs @@ -335,37 +338,37 @@ ||| @ p the equality test ||| @ e the item to search for ||| @ xs the vector to search in-elemBy : (p : a -> a -> Bool) -> (e : a) -> (xs : Vect n a) -> Bool+elemBy : (p : elem -> elem -> Bool) -> (e : elem) -> (xs : Vect len elem) -> Bool elemBy p e []      = False elemBy p e (x::xs) = p e x || elemBy p e xs  ||| Use the default Boolean equality on elements to search for an item ||| @ x what to search for ||| @ xs where to search-elem : Eq a => (x : a) -> (xs : Vect n a) -> Bool+elem : Eq elem => (x : elem) -> (xs : Vect len elem) -> Bool elem = elemBy (==)  ||| Find the association of some key with a user-provided comparison ||| @ p the comparison operator for keys (True if they match) ||| @ e the key to look for-lookupBy : (p : a -> a -> Bool) -> (e : a) -> (xs : Vect n (a, b)) -> Maybe b+lookupBy : (p : key -> key -> Bool) -> (e : key) -> (xs : Vect n (key, val)) -> Maybe val lookupBy p e []           = Nothing lookupBy p e ((l, r)::xs) = if p e l then Just r else lookupBy p e xs  ||| Find the assocation of some key using the default Boolean equality test-lookup : Eq a => a -> Vect n (a, b) -> Maybe b+lookup : Eq key => key -> Vect n (key, val) -> Maybe val lookup = lookupBy (==)  ||| Check if any element of xs is found in elems by a user-provided comparison ||| @ p the comparison operator ||| @ elems the vector to search ||| @ xs what to search for-hasAnyBy : (p : a -> a -> Bool) -> (elems : Vect m a) -> (xs : Vect n a) -> Bool+hasAnyBy : (p : elem -> elem -> Bool) -> (elems : Vect m elem) -> (xs : Vect len elem) -> Bool hasAnyBy p elems []      = False hasAnyBy p elems (x::xs) = elemBy p x elems || hasAnyBy p elems xs  ||| Check if any element of xs is found in elems using the default Boolean equality test-hasAny : Eq a => Vect m a -> Vect n a -> Bool+hasAny : Eq elem => Vect m elem -> Vect len elem -> Bool hasAny = hasAnyBy (==)  --------------------------------------------------------------------------------@@ -374,31 +377,31 @@  ||| Find the first element of the vector that satisfies some test ||| @ p the test to satisfy-find : (p : a -> Bool) -> (xs : Vect n a) -> Maybe a+find : (p : elem -> Bool) -> (xs : Vect len elem) -> Maybe elem find p []      = Nothing find p (x::xs) = if p x then Just x else find p xs  ||| Find the index of the first element of the vector that satisfies some test-findIndex : (a -> Bool) -> Vect n a -> Maybe (Fin n)+findIndex : (elem -> Bool) -> Vect len elem -> Maybe (Fin len) findIndex p []        = Nothing findIndex p (x :: xs) = if p x then Just 0 else map FS (findIndex p xs)  ||| Find the indices of all elements that satisfy some test-findIndices : (a -> Bool) -> Vect m a -> List (Fin m)+findIndices : (elem -> Bool) -> Vect m elem -> List (Fin m) findIndices p []        = [] findIndices p (x :: xs) = let is = map FS $ findIndices p xs                            in if p x then 0 :: is else is -elemIndexBy : (a -> a -> Bool) -> a -> Vect m a -> Maybe (Fin m)+elemIndexBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> Maybe (Fin m) elemIndexBy p e = findIndex $ p e -elemIndex : Eq a => a -> Vect m a -> Maybe (Fin m)+elemIndex : Eq elem => elem -> Vect m elem -> Maybe (Fin m) elemIndex = elemIndexBy (==) -elemIndicesBy : (a -> a -> Bool) -> a -> Vect m a -> List (Fin m)+elemIndicesBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> List (Fin m) elemIndicesBy p e = findIndices $ p e -elemIndices : Eq a => a -> Vect m a -> List (Fin m)+elemIndices : Eq elem => elem -> Vect m elem -> List (Fin m) elemIndices = elemIndicesBy (==)  --------------------------------------------------------------------------------@@ -406,7 +409,7 @@ --------------------------------------------------------------------------------  ||| Find all elements of a vector that satisfy some test-filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)+filter : (elem -> Bool) -> Vect len elem -> (p ** Vect p elem) filter p []      = ( _ ** [] ) filter p (x::xs) =   let (_ ** tail) = filter p xs@@ -416,10 +419,10 @@         (_ ** tail)  ||| Make the elements of some vector unique by some test-nubBy : (a -> a -> Bool) -> Vect n a -> (p ** Vect p a)+nubBy : (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem) nubBy = nubBy' []   where-    nubBy' : Vect m a -> (a -> a -> Bool) -> Vect n a -> (p ** Vect p a)+    nubBy' : Vect m elem -> (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)     nubBy' acc p []      = (_ ** [])     nubBy' acc p (x::xs) with (elemBy p x acc)       | True  = nubBy' acc p xs@@ -427,16 +430,16 @@         | (_ ** tail) = (_ ** x::tail)  ||| Make the elements of some vector unique by the default Boolean equality-nub : Eq a => Vect n a -> (p ** Vect p a)+nub : Eq elem => Vect len elem -> (p ** Vect p elem) nub = nubBy (==) -deleteBy : (a -> a -> Bool) -> a -> Vect n a -> (p ** Vect p a)+deleteBy : (elem -> elem -> Bool) -> elem -> Vect len elem -> (p ** Vect p elem) deleteBy _  _ []      = (_ ** []) deleteBy eq x (y::ys) =   let (len ** zs) = deleteBy eq x ys   in if x `eq` y then (_ ** ys) else (S len ** y ::zs) -delete : (Eq a) => a -> Vect n a -> (p ** Vect p a)+delete : (Eq elem) => elem -> Vect len elem -> (p ** Vect p elem) delete = deleteBy (==)  --------------------------------------------------------------------------------@@ -448,10 +451,10 @@ ||| It is equivalent to (take n xs, drop n xs) ||| @ n   the index to split at ||| @ xs  the Vect to split in two-splitAt : (n : Nat) -> (xs : Vect (n + m) a) -> (Vect n a, Vect m a)+splitAt : (n : Nat) -> (xs : Vect (n + m) elem) -> (Vect n elem, Vect m elem) splitAt n xs = (take n xs, drop n xs) -partition : (a -> Bool) -> Vect n a -> ((p ** Vect p a), (q ** Vect q a))+partition : (elem -> Bool) -> Vect len elem -> ((p ** Vect p elem), (q ** Vect q elem)) partition p []      = ((_ ** []), (_ ** [])) partition p (x::xs) =   let ((leftLen ** lefts), (rightLen ** rights)) = partition p xs in@@ -464,29 +467,29 @@ -- Predicates -------------------------------------------------------------------------------- -isPrefixOfBy : (a -> a -> Bool) -> Vect m a -> Vect n a -> Bool+isPrefixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool isPrefixOfBy p [] right        = True isPrefixOfBy p left []         = False isPrefixOfBy p (x::xs) (y::ys) = p x y && isPrefixOfBy p xs ys -isPrefixOf : Eq a => Vect m a -> Vect n a -> Bool+isPrefixOf : Eq elem => Vect m elem -> Vect len elem -> Bool isPrefixOf = isPrefixOfBy (==) -isSuffixOfBy : (a -> a -> Bool) -> Vect m a -> Vect n a -> Bool+isSuffixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right) -isSuffixOf : Eq a => Vect m a -> Vect n a -> Bool+isSuffixOf : Eq elem => Vect m elem -> Vect len elem -> Bool isSuffixOf = isSuffixOfBy (==)  -------------------------------------------------------------------------------- -- Conversions -------------------------------------------------------------------------------- -maybeToVect : Maybe a -> (p ** Vect p a)+maybeToVect : Maybe elem -> (p ** Vect p elem) maybeToVect Nothing  = (_ ** []) maybeToVect (Just j) = (_ ** [j]) -vectToMaybe : Vect n a -> Maybe a+vectToMaybe : Vect len elem -> Maybe elem vectToMaybe []      = Nothing vectToMaybe (x::xs) = Just x @@ -494,25 +497,25 @@ -- Misc -------------------------------------------------------------------------------- -catMaybes : Vect n (Maybe a) -> (p ** Vect p a)+catMaybes : Vect n (Maybe elem) -> (p ** Vect p elem) catMaybes []             = (_ ** []) catMaybes (Nothing::xs)  = catMaybes xs catMaybes ((Just j)::xs) =   let (_ ** tail) = catMaybes xs    in (_ ** j::tail) -diag : Vect n (Vect n a) -> Vect n a+diag : Vect len (Vect len elem) -> Vect len elem diag []             = [] diag ((x::xs)::xss) = x :: diag (map tail xss) -range : {n : Nat} -> Vect n (Fin n)-range {n=Z}   = []-range {n=S _} = FZ :: map FS range+range : {len : Nat} -> Vect len (Fin len)+range {len=Z}   = []+range {len=S _} = FZ :: map FS range  ||| Transpose a Vect of Vects, turning rows into columns and vice versa. ||| ||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.-transpose : {n : Nat} -> Vect m (Vect n a) -> Vect n (Vect m a)+transpose : {n : Nat} -> Vect m (Vect n elem) -> Vect n (Vect m elem) transpose []        = replicate _ [] transpose (x :: xs) = zipWith (::) x (transpose xs) @@ -527,7 +530,7 @@  ||| This monad is different from the List monad, (>>=) ||| uses the diagonal.-implementation Monad (Vect n) where+implementation Monad (Vect len) where     m >>= f = diag (map f m)  implementation Traversable (Vect n) where@@ -538,14 +541,14 @@ -- Show -------------------------------------------------------------------------------- -implementation Show a => Show (Vect n a) where+implementation Show elem => Show (Vect len elem) where     show = show . toList  -------------------------------------------------------------------------------- -- Properties -------------------------------------------------------------------------------- -vectConsCong : (x : a) -> (xs : Vect n a) -> (ys : Vect m a) -> (xs = ys) -> (x :: xs = x :: ys)+vectConsCong : (x : elem) -> (xs : Vect len elem) -> (ys : Vect m elem) -> (xs = ys) -> (x :: xs = x :: ys) vectConsCong x xs xs Refl = Refl  vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs@@ -553,7 +556,10 @@ vectNilRightNeutral (x :: xs) =   vectConsCong _ _ _ (vectNilRightNeutral xs) -vectAppendAssociative : (x : Vect xLen a) -> (y : Vect yLen a) -> (z : Vect zLen a) -> x ++ (y ++ z) = (x ++ y) ++ z+vectAppendAssociative : (xs : Vect xLen elem) ->+                        (ys : Vect yLen elem) ->+                        (zs : Vect zLen elem) ->+                        xs ++ (ys ++ zs) = (xs ++ ys) ++ zs vectAppendAssociative [] y z = Refl vectAppendAssociative (x :: xs) ys zs =   vectConsCong _ _ _ (vectAppendAssociative xs ys zs)@@ -599,7 +605,7 @@ noEmptyElem Here impossible  Uninhabited (Elem x []) where-  uninhabited = noEmptyElem +  uninhabited = noEmptyElem  ||| An item not in the head and not in the tail is not in the Vect at all neitherHereNorThere : {x, y : a} -> {xs : Vect n a} -> Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))@@ -634,7 +640,7 @@ ||| length in its type, otherwise return Nothing ||| @len the required length ||| @xs the vector with the desired length--- Needs to be Maybe rather than Dec, because if 'n' is unequal to m, we +-- Needs to be Maybe rather than Dec, because if 'n' is unequal to m, we -- only know we don't know how to make a Vect n a, not that one can't exist. exactLength : {m : Nat} -> -- expected at run-time               (len : Nat) -> (xs : Vect m a) -> Maybe (Vect len a)@@ -654,4 +660,3 @@          = Just (0 ** xs)   overLength {m = plus n (S x)} n xs | (CmpGT x)          = Just (S x ** rewrite plusCommutative (S x) n in xs)-

@@ -4,8 +4,9 @@ build: 	$(IDRIS) --build ${PKG}.ipkg -install: +install: 	$(IDRIS) --install ${PKG}.ipkg+	${IDRIS} --installdoc ${PKG}.ipkg  clean: 	$(IDRIS) --clean ${PKG}.ipkg@@ -21,4 +22,4 @@ linecount: 	find . -name '*.idr' | xargs wc -l -.PHONY: build install clean rebuild linecount+.PHONY: build install clean rebuild linecount doc doc_clean

@@ -16,10 +16,13 @@      MkPID : (pid : Ptr) -> PID  ||| Spawn a process in a new thread, returning the process ID+||| Returns `Nothing` if there are not enough resources to create the new thread export-spawn : (process : IO ()) -> IO PID+spawn : (process : IO ()) -> IO (Maybe PID) spawn proc = do pid <- fork proc-                pure (MkPID pid)+                if !(nullPtr pid)+                   then pure Nothing+                   else pure (Just (MkPID pid))  ||| Create a channel which connects this process to another process export@@ -61,3 +64,7 @@ unsafeRecv : (expected : Type) -> Channel -> IO (Maybe expected) unsafeRecv a (MkConc pid ch_id) = getMsgFrom {a} pid ch_id +||| Exit the thread immediately+export+stopThread : IO a+stopThread = Raw.stopThread 

@@ -106,3 +106,9 @@              foreign FFI_C "idris_freeMsg" (Ptr -> IO ()) m              pure (Just x) +stopThread : IO a+stopThread = do vm <- getMyVM+                MkRaw res <- foreign FFI_C "idris_stopThread" (Ptr -> IO (Raw a)) vm+                pure res++

@@ -0,0 +1,9 @@+module Data.Fin.Extra++import Data.Fin++||| Proof that an element **n** of Fin **m** , when converted to Nat is smaller than the bound **m**.+public export+elemSmallerThanBound : (n : Fin m) -> LTE (finToNat n) m+elemSmallerThanBound FZ = LTEZero+elemSmallerThanBound (FS x) = LTESucc (elemSmallerThanBound x)

@@ -4,8 +4,9 @@ build: 	$(IDRIS) --build ${PKG}.ipkg -install: +install: 	$(IDRIS) --install ${PKG}.ipkg+	${IDRIS} --installdoc ${PKG}.ipkg  clean: 	$(IDRIS) --clean ${PKG}.ipkg@@ -21,4 +22,4 @@ linecount: 	find . -name '*.idr' | xargs wc -l -.PHONY: build install clean rebuild linecount+.PHONY: build install clean rebuild linecount doc doc_clean

@@ -25,4 +25,6 @@            Network.Cgi, Network.Socket, -          System.Concurrency.Process+          System.Concurrency.Process,++          Data.Fin.Extra

@@ -9,6 +9,7 @@  install: 	$(IDRIS) --install ${PKG}.ipkg+	${IDRIS} --installdoc ${PKG}.ipkg  rebuild: clean build 

@@ -160,7 +160,8 @@ par (Delay x) = x  ||| Assert to the totality checker that y is always structurally smaller than-||| x (which is typically a pattern argument)+||| x (which is typically a pattern argument, and *must* be in normal form+||| for this to work) ||| @ x the larger value (typically a pattern argument) ||| @ y the smaller value (typically an argument to a recursive call) assert_smaller : (x : a) -> (y : b) -> b

@@ -4,8 +4,9 @@ build: 	$(IDRIS) --build ${PKG}.ipkg -install: +install: 	$(IDRIS) --install ${PKG}.ipkg+	${IDRIS} --installdoc ${PKG}.ipkg  clean: 	$(IDRIS) --clean ${PKG}.ipkg

@@ -156,8 +156,15 @@ total natEnumFromThenTo' : Nat -> Nat -> Nat -> List Nat natEnumFromThenTo' _ Z       _ = [] natEnumFromThenTo' n (S inc) m = map (plus n . (* (S inc))) (natRange (S (divNatNZ (minus m n) (S inc) SIsNotZ)))+ total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat-natEnumFromThenTo n next m = natEnumFromThenTo' n (minus next n) m+natEnumFromThenTo n next m = if n == m then [n]+                             else if n < m then natEnumFromThenTo' n (minus next n) m+                             else case minus n next of+                                  Z => []+                                  S step => List.reverse . map (+ (modNatNZ (minus n m) (S step) SIsNotZ)) $ natEnumFromThenTo' m (minus n next) n+    where modNatNZ : Nat -> (m : Nat) -> Not (m = 0) -> Nat+          modNatNZ n m nz = minus n $ mult m $ divNatNZ n m nz  interface Enum a where   total pred : a -> a@@ -197,8 +204,9 @@           go' n (x :: xs) = n + cast x :: go' n xs           go : Integer -> Integer -> List Integer           go n m = go' n (natRange (S (cast {to = Nat} (m - n))))-  enumFromThenTo _ 0   _ = []-  enumFromThenTo n next m = go (natRange (S (divNatNZ (fromInteger (abs (m - n))) (S (fromInteger ((abs (next - n)) - 1))) SIsNotZ)))+  enumFromThenTo n next m = if n == m then [n]+                            else if next - n == 0 || next - n < 0 /= m - n < 0 then []+                            else go (natRange (S (divNatNZ (fromInteger (abs (m - n))) (S (fromInteger ((abs (next - n)) - 1))) SIsNotZ)))     where go : List Nat -> List Integer           go [] = []           go (x :: xs) = n + (cast x * (next - n)) :: go xs@@ -217,8 +225,9 @@           go : Int -> Int -> List Int           go n m = go' [] (cast {to = Nat} (m - n)) m   enumFromThen n inc = n :: enumFromThen (inc + n) inc-  enumFromThenTo _ 0   _ = []-  enumFromThenTo n next m = go (natRange (S (divNatNZ (cast {to=Nat} (abs (m - n))) (S (cast {to=Nat} ((abs (next - n)) - 1))) SIsNotZ)))+  enumFromThenTo n next m = if n == m then [n]+                            else if next - n == 0 || next - n < 0 /= m - n < 0 then []+                            else go (natRange (S (divNatNZ (cast {to=Nat} (abs (m - n))) (S (cast {to=Nat} ((abs (next - n)) - 1))) SIsNotZ)))     where go : List Nat -> List Int           go [] = []           go (x :: xs) = n + (cast x * (next - n)) :: go xs

@@ -89,6 +89,16 @@ getChar : IO Char getChar = map cast $ foreign FFI_C "getchar" (IO Int) +||| Disables buffering in both stdin and stdout:+||| so that output is written immediately (never stored in the buffer)+||| and the next input item is read and returned+|||+||| this is useful to circumvent problems with IO on some Windows systems+||| where stdout output right before a prompt is only shown after+||| the input-line from stdin is produced+disableBuffering : IO ()+disableBuffering = foreign FFI_C "idris_disableBuffering" (IO ())+ ||| Get the command-line arguments that the program was called with. partial getArgs : IO (List String)

@@ -7,6 +7,7 @@ import Prelude.Cast import Prelude.Interfaces import Prelude.Foldable+import Prelude.Uninhabited  %access public export %default total@@ -37,6 +38,14 @@ ||| Proof that some `Maybe` is actually `Just` data IsJust : Maybe a -> Type where   ItIsJust : IsJust (Just x)++Uninhabited (IsJust Nothing) where+  uninhabited ItIsJust impossible++||| Decide whether a 'Maybe' is 'Just'+isItJust : (v : Maybe a) -> Dec (IsJust v)+isItJust (Just x) = Yes ItIsJust+isItJust Nothing = No absurd  -------------------------------------------------------------------------------- -- Misc

@@ -310,9 +310,19 @@ -- Division and modulus -------------------------------------------------------------------------------- +||| The proof that no successor of a natural number can be zero.+|||+||| ```idris example+||| modNatNZ 10 3 SIsNotZ+||| ``` SIsNotZ : {x: Nat} -> (S x = Z) -> Void SIsNotZ Refl impossible +||| Modulus function where the divisor is not zero.+|||+||| ```idris example+||| modNatNZ 100 2 SIsNotZ+||| ``` modNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat modNatNZ left Z         p = void (p Refl) modNatNZ left (S right) _ = mod' left left right@@ -329,6 +339,11 @@ modNat : Nat -> Nat -> Nat modNat left (S right) = modNatNZ left (S right) SIsNotZ +||| Division where the divisor is not zero.+|||+||| ```idris example+||| divNatNZ 100 2 SIsNotZ+||| ``` divNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat divNatNZ left Z         p = void (p Refl) divNatNZ left (S right) _ = div' left left right

@@ -46,7 +46,7 @@   ||| @ x the value to convert   partial   show : (x : ty) -> String-  show = showPrec Open+  show x = showPrec Open x -- Eta expand to help totality checker    ||| Convert a value to its `String` representation in a certain precedence   ||| context.@@ -63,7 +63,7 @@   ||| @ x the value to convert   partial   showPrec : (d : Prec) -> (x : ty) -> String-  showPrec _ = show+  showPrec _ x = show x  ||| Surround a `String` with parentheses depending on a condition. |||

@@ -328,7 +328,7 @@ toLower x with (strM x)   toLower ""             | StrNil = ""   toLower (strCons c cs) | (StrCons c cs) =-    strCons (toLower c) (toLower (assert_smaller (strCons c cs) cs))+    strCons (toLower c) (toLower (assert_smaller (prim__strCons c cs) cs))  ||| Uppercases all characters in the string. |||@@ -339,7 +339,7 @@ toUpper x with (strM x)   toUpper ""             | StrNil = ""   toUpper (strCons c cs) | (StrCons c cs) =-    strCons (toUpper c) (toUpper (assert_smaller (strCons c cs) cs ))+    strCons (toUpper c) (toUpper (assert_smaller (prim__strCons c cs) cs ))  -------------------------------------------------------------------------------- -- Predicates

@@ -9,6 +9,7 @@  install: 	$(IDRIS) --install ${PKG}.ipkg+	${IDRIS} --installdoc ${PKG}.ipkg  rebuild: clean build 

@@ -3,7 +3,7 @@ import Language.Reflection.Utils import Data.Vect -import Pruviloj.Core+import public Pruviloj.Core import Pruviloj.Internals.TyConInfo import Pruviloj.Internals import Pruviloj.Renamers@@ -63,7 +63,7 @@                 focus ihT                 attack                 for_ {b=()} argArgs $ \(n, b) =>-                  forall n (getBinderTy b)+                  forall n (binderTy b)                 let argTm : Raw = mkApp (Var recArg) (map (Var . fst) argArgs)                 argTmTy <- forget (snd !(check !getEnv argTm))                 argHoles <- apply (Var motiveName)@@ -239,7 +239,7 @@    where bindLam : List (TTName, Binder Raw) -> Raw -> Raw         bindLam [] x = x-        bindLam ((n, b)::rest) x = RBind n (Lam (getBinderTy b)) $ bindLam rest x+        bindLam ((n, b)::rest) x = RBind n (Lam (binderTy b)) $ bindLam rest x  getElimClauses : TyConInfo -> (elimn : TTName) ->                  List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))

@@ -1,7 +1,7 @@ ||| Internal details of the library, not for public consumption. module Pruviloj.Internals -+import Language.Reflection.Utils import Pruviloj.Core import Pruviloj.Renamers @@ -50,16 +50,6 @@ extractBinders tm = ([], tm)  -||| Get the type annotation from a binder-getBinderTy : Binder t -> t-getBinderTy (Lam t) = t-getBinderTy (Pi t _) = t-getBinderTy (Let t _) = t-getBinderTy (Hole t) = t-getBinderTy (GHole t) = t-getBinderTy (Guess t _) = t-getBinderTy (PVar t) = t-getBinderTy (PVTy t) = t  ||| Map a list `[x1, x2, ..., xn]` to `[(0, x1), (1, x2), ..., (n-1, xn)]` enumerate : List a -> List (Nat, a)@@ -70,11 +60,11 @@  bindPats : List (TTName, Binder Raw) -> Raw -> Raw bindPats [] res = res-bindPats ((n, b)::bs) res = RBind n (PVar (getBinderTy b)) $ bindPats bs res+bindPats ((n, b)::bs) res = RBind n (PVar (binderTy b)) $ bindPats bs res  bindPatTys : List (TTName, Binder Raw) -> Raw -> Raw bindPatTys [] res = res-bindPatTys ((n, b)::bs) res = RBind n (PVTy (getBinderTy b)) $ bindPatTys bs res+bindPatTys ((n, b)::bs) res = RBind n (PVTy (binderTy b)) $ bindPatTys bs res   ||| Helper for elaborating pattern clauses. This helper takes care of

@@ -1,4 +1,4 @@-module Pruviloj.Derive.TyConInfo+module Pruviloj.Internals.TyConInfo  import Pruviloj.Core import Pruviloj.Internals

@@ -1,17 +1,22 @@ module Main where -import Control.Monad ( when )-import System.Exit ( exitSuccess )+import System.Exit ( ExitCode(..), exitWith, exitSuccess ) +import Control.Monad ( unless, when, (>=>) )+import Data.Maybe    ( fromMaybe )+import Data.Foldable ( foldrM )+ import Idris.AbsSyntax-import Idris.Error import Idris.CmdOptions-import Idris.Info+import Idris.Error import Idris.Info.Show-import Idris.Package import Idris.Main+import Idris.Package +import Util.System (setupBundledCC)+ import Util.System ( setupBundledCC )+import System.Exit ( ExitCode(..), exitWith)  processShowOptions :: [Opt] -> Idris () processShowOptions opts = runIO $ do@@ -19,7 +24,8 @@   when (ShowLoggingCats `elem` opts)  $ showExitIdrisLoggingCategories   when (ShowIncs `elem` opts)         $ showExitIdrisFlagsInc   when (ShowLibs `elem` opts)         $ showExitIdrisFlagsLibs-  when (ShowLibdir `elem` opts)       $ showExitIdrisLibDir+  when (ShowLibDir `elem` opts)       $ showExitIdrisLibDir+  when (ShowDocDir `elem` opts)       $ showExitIdrisDocDir   when (ShowPkgs `elem` opts)         $ showExitIdrisInstalledPackages  check :: [Opt] -> (Opt -> Maybe a) -> ([a] -> Idris ()) -> Idris ()@@ -31,7 +37,8 @@  processClientOptions :: [Opt] -> Idris () processClientOptions opts = check opts getClient $ \fs -> case fs of-  (c:_) -> do+  []      -> ifail "No --client argument. This indicates a bug. Please report."+  (c : _) -> do     setVerbose False     setQuiet True     case getPort opts of@@ -48,7 +55,13 @@   check opts getPkgMkDoc $ \fs -> runIO $ do     mapM_ (documentPkg opts) fs   check opts getPkgTest $ \fs -> runIO $ do-    mapM_ (testPkg opts) fs++    codes <- mapM (testPkg opts) fs+    -- check if any of the tests exited with an exit code other+    -- than zero; if they did, exit with exit code 1+    unless (null $ filter (/= ExitSuccess) codes) $+       exitWith (ExitFailure 1)+   check opts getPkg $ \fs -> runIO $ do     mapM_ (buildPkg opts (WarnOnly `elem` opts)) fs   check opts getPkgREPL $ \fs -> case fs of

@@ -1,6 +1,6 @@ .\" Manpage for Idris. .\" Contact <> to correct errors or typos.-.TH man 1 "25 March 2016" "0.12.3" "Idris man page"+.TH man 1 "28 November 2016" "0.99" "Idris man page" .SH NAME idris -\ a general purpose pure functional programming language with dependent types. .SH SYNOPSIS@@ -13,17 +13,29 @@ evaluation. Its features are influenced by Haskell and ML.  + Full dependent types with dependent pattern matching+ + Simple case expressions, where-clauses, with-rule+ + Pattern matching let- and lambda-bindings+ + Overloading via Interfaces (Type class-like), Monad comprehensions+ + do-notation, idiom brackets+ + Syntactic conveniences for lists, tuples, dependent pairs+ + Totality checking+ + Coinductive types+ + Indentation significant syntax, Extensible syntax+ + Tactic based theorem proving (influenced by Coq)+ + Cumulative universes+ + Simple Foreign Function Interface+ + Hugs style interactive environment  It is important to note that Idris is first and foremost a research tool

@@ -1,26 +1,64 @@ #!/bin/sh -VERSION=$1+set -euo pipefail -echo "Building version-$VERSION\n\n"-echo "Have you: set the release flag, checked the demos and the tutorial?"-read $foo+if [ "$#" -lt 1 ]; then+    echo "Usage $0 [version number] ?[idris bin location]"+    echo ""+    echo "The first argument is the version number"+    echo ""+    echo "The second argument is optional, and used to point to a"+    echo "custom location in which idris was recently built i.e."+    echo "withing .stack-work or .cabal-sandbox. The location must"+    echo "be given relative to the project root of a package in the "+    echo "libs/ directory."+    exit 1+fi +VERSION=${1:-}++echo "==> Building version-$VERSION"+echo ""+echo "Q: Have you: (a) set the release flag & (b) checked the demos and the tutorial?"+read ${FOO:-}+ git tag v$VERSION -a +echo "==> Building Source Distribution" cabal sdist  # Generate Idris library docs and put them in lib_docs.tar.gz in the root-make lib_doc+echo "==> Generating API Documentation."+echo "==> Determining version of Idris to use."+if [ -z ${2+x} ];+then+    echo "==> Using default location.";+    make lib_doc+else+    echo "==> Using custom location.";+    make -C libs IDRIS=$2 doc+fi+ DOCDIR=`mktemp -d /tmp/docsXXXXX`+ cp -r libs/base/base_doc "$DOCDIR" cp -r libs/prelude/prelude_doc "$DOCDIR" cp -r libs/effects/effects_doc "$DOCDIR" cp -r libs/contrib/contrib_doc "$DOCDIR"+ tar -czvf lib_docs.tar.gz -C "$DOCDIR" prelude_doc base_doc effects_doc contrib_doc +echo "==> Building Binaries" cabal configure --prefix=/usr/local+ cabal build++echo "==> Creating Package"+mkdir -p /tmp/idris-pkg/+ cabal copy --destdir=/tmp/idris-pkg/-pkgbuild --id org.idris-lang --root /tmp/idris-pkg/ idris-$VERSION.pkg  +pkgbuild --identifier org.idris-lang \+         --version "v$VERSION"       \+         --root /tmp/idris-pkg/      \+         idris-$VERSION.pkg

@@ -748,11 +748,22 @@      callvm->processes++; -    pthread_create(&t, &attr, runThread, td);+    int ok = pthread_create(&t, &attr, runThread, td); //    usleep(100);-    return vm;+    if (ok == 0) {+        return vm;+    } else {+        terminate(vm);+        return NULL;+    } } +void* idris_stopThread(VM* vm) {+    close_vm(vm);+    pthread_exit(NULL);+    return NULL;+}+ // VM is assumed to be a different vm from the one x lives on  VAL doCopyTo(VM* vm, VAL x) {@@ -1069,6 +1080,11 @@  const char* idris_getArg(int i) {     return __idris_argv[i];+}++void idris_disableBuffering() {+  setvbuf(stdin, NULL, _IONBF, 0);+  setvbuf(stdout, NULL, _IONBF, 0); }  void stackOverflow() {

@@ -309,6 +309,7 @@ void init_signals();  void* vmThread(VM* callvm, func f, VAL arg);+void* idris_stopThread(VM* vm);  // Copy a structure to another vm's heap VAL copyTo(VM* newVM, VAL x);@@ -392,6 +393,9 @@  int idris_numArgs(); const char *idris_getArg(int i);++// disable stdin/stdout buffering+void idris_disableBuffering();  // Handle stack overflow. // Just reports an error and exits.

@@ -20,13 +20,13 @@                       (Node Leaf "Bob" Leaf))  treeTagAux : BTree a -> { [STATE Int] } Eff (BTree (Int, a))-treeTagAux Leaf = return Leaf+treeTagAux Leaf = pure Leaf treeTagAux (Node l x r)     = do l' <- treeTagAux l          i <- get          put (i + 1)          r' <- treeTagAux r-         return (Node l' (i, x) r')+         pure (Node l' (i, x) r')  treeTag : (i : Int) -> BTree a -> BTree (Int, a) treeTag i x = runPure (do put i

@@ -1,7 +1,7 @@ m_add : Maybe Int -> Maybe Int -> Maybe Int m_add x y = do x' <- x -- Extract value from x                y' <- y -- Extract value from y-               return (x' + y') -- Add them+               pure (x' + y') -- Add them  m_add' : Maybe Int -> Maybe Int -> Maybe Int m_add' x y = [ x' + y' | x' <- x, y' <- y ]

@@ -7,9 +7,9 @@ -} module IRTS.BCImp where +import Idris.Core.TT import IRTS.Lang import IRTS.Simplified-import Idris.Core.TT  data Reg = RVal | L Int 

@@ -21,10 +21,11 @@ module IRTS.Bytecode where  +import Idris.Core.TT+import IRTS.Defunctionalise import IRTS.Lang import IRTS.Simplified-import IRTS.Defunctionalise-import Idris.Core.TT+ import Data.Maybe  data Reg = RVal | L Int | T Int | Tmp

@@ -8,27 +8,27 @@ module IRTS.CodegenC (codegenC) where  import Idris.AbsSyntax+import Idris.Core.TT import IRTS.Bytecode+import IRTS.CodegenCommon+import IRTS.Defunctionalise import IRTS.Lang import IRTS.Simplified-import IRTS.Defunctionalise import IRTS.System-import IRTS.CodegenCommon-import Idris.Core.TT+ import Util.System -import Numeric-import Data.Char+import Control.Monad import Data.Bits+import Data.Char import Data.List (intercalate, nubBy)-import System.Process+import Debug.Trace+import Numeric+import System.Directory import System.Exit+import System.FilePath ((<.>), (</>)) import System.IO-import System.Directory-import System.FilePath ((</>), (<.>))-import Control.Monad--import Debug.Trace+import System.Process  codegenC :: CodeGenerator codegenC ci = do codegenC' (simpleDecls ci)@@ -66,8 +66,8 @@          let h = concatMap toDecl (map fst bc)          let cc = concatMap (uncurry toC) bc          let hi = concatMap ifaceC (concatMap getExp exports)-         d <- getDataDir-         mprog <- readFile (d </> "rts" </> "idris_main" <.> "c")+         d <- getIdrisCRTSDir+         mprog <- readFile (d </> "idris_main" <.> "c")          let cout = headers incs ++ debug dbg ++ h ++ wrappers ++ cc ++                      (if (exec == Executable) then mprog else hi)          case exec of

@@ -8,11 +8,11 @@ -} module IRTS.CodegenCommon where -import GHC.Generics (Generic)- import Idris.Core.TT-import IRTS.Simplified import IRTS.Defunctionalise+import IRTS.Simplified++import GHC.Generics (Generic)  data DbgLevel = NONE | DEBUG | TRACE deriving Eq data OutputType = Raw | Object | Executable deriving (Eq, Show, Generic)

@@ -5,44 +5,41 @@ License     : BSD3 Maintainer  : The Idris Community. -}-{-# LANGUAGE PatternGuards #-}-{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE OverloadedStrings, PatternGuards #-} module IRTS.CodegenJavaScript (codegenJavaScript                              , codegenNode                              , JSTarget(..)                              ) where -import IRTS.JavaScript.AST- import Idris.AbsSyntax hiding (TypeCase)+import Idris.Core.TT import IRTS.Bytecode-import IRTS.Lang+import IRTS.CodegenCommon+import IRTS.Defunctionalise import IRTS.Exports+import IRTS.JavaScript.AST+import IRTS.Lang import IRTS.Simplified-import IRTS.Defunctionalise-import IRTS.CodegenCommon-import Idris.Core.TT import IRTS.System import Util.System +import Control.Applicative (pure, (<$>), (<*>)) import Control.Arrow import Control.Monad (mapM)-import Control.Applicative ((<$>), (<*>), pure) import Control.Monad.RWS hiding (mapM) import Control.Monad.State import Data.Char-import Numeric import Data.List+import qualified Data.Map.Strict as M import Data.Maybe-import Data.Word+import qualified Data.Text as T+import qualified Data.Text.IO as TIO import Data.Traversable hiding (mapM)-import System.IO+import Data.Word+import Numeric import System.Directory import System.FilePath--import qualified Data.Map.Strict as M-import qualified Data.Text as T-import qualified Data.Text.IO as TIO+import System.IO   data CompileInfo = CompileInfo { compileInfoApplyCases  :: [Int]@@ -121,27 +118,27 @@   -> OutputType   -> IO () codegenJS_all target definitions includes libs filename exports outputType = do-  let bytecode = map toBC definitions-  let info = initCompileInfo bytecode-  let js = concatMap (translateDecl info) bytecode-  let full = concatMap processFunction js+  let bytecode      = map toBC definitions+  let info          = initCompileInfo bytecode+  let js            = concatMap (translateDecl info) bytecode+  let full          = concatMap processFunction js   let exportedNames = map translateName ((getExpNames exports) ++ [sUN "call__IO"])-  let code = deadCodeElim exportedNames full-  let ext = takeExtension filename-  let isHtml = target == JavaScript && ext == ".html"-  let htmlPrologue = T.pack "<!doctype html><html><head><script>\n"-  let htmlEpilogue = T.pack "\n</script></head><body></body></html>"-  let (cons, opt) = optimizeConstructors code-  let (header, rt) = case target of-                          Node -> ("#!/usr/bin/env node\n", "-node")+  let code          = deadCodeElim exportedNames full+  let ext           = takeExtension filename+  let isHtml        = target == JavaScript && ext == ".html"+  let htmlPrologue  = T.pack "<!doctype html><html><head><script>\n"+  let htmlEpilogue  = T.pack "\n</script></head><body></body></html>"+  let (cons, opt)   = optimizeConstructors code+  let (header, rt)   = case target of+                          Node       -> ("#!/usr/bin/env node\n", "-node")                           JavaScript -> ("", "-browser")    included   <- concat <$> getIncludes includes-  path       <- (++) <$> getDataDir <*> (pure "/jsrts/")-  idrRuntime <- readFile $ path ++ "Runtime-common.js"-  tgtRuntime <- readFile $ concat [path, "Runtime", rt, ".js"]+  path       <- getIdrisJSRTSDir+  idrRuntime <- readFile $ path </> "Runtime-common.js"+  tgtRuntime <- readFile $ path </> concat ["Runtime", rt, ".js"]   jsbn       <- if compileInfoNeedsBigInt info-                   then readFile $ path ++ "jsbn/jsbn.js"+                   then readFile $ path </> "jsbn/jsbn.js"                    else return ""   let runtime = (  header                 ++ includeLibs libs

@@ -5,55 +5,50 @@ License     : BSD3 Maintainer  : The Idris Community. -}-{-# LANGUAGE PatternGuards, TypeSynonymInstances, CPP #-}+{-# LANGUAGE CPP, PatternGuards, TypeSynonymInstances #-}  module IRTS.Compiler(compile, generate) where -import IRTS.Lang-import IRTS.LangOpts-import IRTS.Defunctionalise-import IRTS.Simplified-import IRTS.CodegenCommon-import IRTS.CodegenC-import IRTS.DumpBC-import IRTS.CodegenJavaScript-import IRTS.Inliner-import IRTS.Exports-import IRTS.Portable- import Idris.AbsSyntax import Idris.AbsSyntaxTree import Idris.ASTUtils+import Idris.Core.CaseTree+import Idris.Core.Evaluate+import Idris.Core.TT import Idris.Erasure import Idris.Error import Idris.Output--import Debug.Trace--import Idris.Core.TT-import Idris.Core.Evaluate-import Idris.Core.CaseTree+import IRTS.CodegenC+import IRTS.CodegenCommon+import IRTS.CodegenJavaScript+import IRTS.Defunctionalise+import IRTS.DumpBC+import IRTS.Exports+import IRTS.Inliner+import IRTS.Lang+import IRTS.LangOpts+import IRTS.Portable+import IRTS.Simplified -import Control.Category import Prelude hiding (id, (.))  import Control.Applicative+import Control.Category import Control.Monad.State--import           Data.Maybe-import           Data.List-import           Data.Ord-import           Data.IntSet (IntSet)-import qualified Data.IntSet          as IS-import qualified Data.Map             as M-import qualified Data.Set             as S--import System.Process-import System.IO-import System.Exit+import Data.IntSet (IntSet)+import qualified Data.IntSet as IS+import Data.List+import qualified Data.Map as M+import Data.Maybe+import Data.Ord+import qualified Data.Set as S+import Debug.Trace import System.Directory import System.Environment-import System.FilePath ((</>), addTrailingPathSeparator)+import System.Exit+import System.FilePath (addTrailingPathSeparator, (</>))+import System.IO+import System.Process  -- |  Compile to simplified forms and return CodegenInfo compile :: Codegen -> FilePath -> Maybe Term -> Idris CodegenInfo

@@ -24,15 +24,15 @@                           , module IRTS.Lang                           ) where -import IRTS.Lang-import Idris.Core.TT import Idris.Core.CaseTree+import Idris.Core.TT+import IRTS.Lang -import Debug.Trace-import Data.Maybe-import Data.List import Control.Monad import Control.Monad.State+import Data.List+import Data.Maybe+import Debug.Trace  data DExp = DV LVar           | DApp Bool Name [DExp] -- True = tail call

@@ -7,11 +7,11 @@ -} module IRTS.DumpBC where +import Idris.Core.TT+import IRTS.Bytecode import IRTS.Lang import IRTS.Simplified-import Idris.Core.TT -import IRTS.Bytecode import Data.List  interMap :: [a] -> [b] -> (a -> [b]) -> [b]

@@ -9,9 +9,9 @@ module IRTS.Exports(findExports, getExpNames) where  import Idris.AbsSyntax-import Idris.Core.TT import Idris.Core.CaseTree import Idris.Core.Evaluate+import Idris.Core.TT import Idris.Error import IRTS.Lang 

@@ -8,7 +8,6 @@ module IRTS.Inliner where  import Idris.Core.TT- import IRTS.Defunctionalise  inline :: DDefs -> DDefs

@@ -5,14 +5,12 @@ License     : BSD3 Maintainer  : The Idris Community. -}-{-# LANGUAGE PatternGuards #-}-{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE OverloadedStrings, PatternGuards #-} module IRTS.JavaScript.AST where -import Data.Word import Data.Char (isDigit)- import qualified Data.Text as T+import Data.Word  data JSType = JSIntTy             | JSStringTy

@@ -5,16 +5,15 @@ License     : BSD3 Maintainer  : The Idris Community. -}-{-# LANGUAGE PatternGuards, DeriveFunctor, DeriveGeneric #-}+{-# LANGUAGE DeriveFunctor, DeriveGeneric, PatternGuards #-}  module IRTS.Lang where -import Control.Monad.State hiding (lift)-import Control.Applicative hiding (Const)--import Idris.Core.TT import Idris.Core.CaseTree+import Idris.Core.TT +import Control.Applicative hiding (Const)+import Control.Monad.State hiding (lift) import Data.List import Debug.Trace import GHC.Generics (Generic)@@ -319,7 +318,7 @@                                        LCon lv t cn args' lsubst n new (LOp op args) = let args' = map (lsubst n new) args in                                  LOp op args'-lsubst n new (LForeign fd rd args) +lsubst n new (LForeign fd rd args)      = let args' = map (\(d, a) -> (d, lsubst n new a)) args in            LForeign fd rd args' lsubst n new (LCase t e alts) = let e' = lsubst n new e

@@ -5,16 +5,16 @@ License     : BSD3 Maintainer  : The Idris Community. -}-{-# LANGUAGE PatternGuards, DeriveFunctor #-}+{-# LANGUAGE DeriveFunctor, PatternGuards #-}  module IRTS.LangOpts where -import Control.Monad.State hiding (lift)-import Control.Applicative hiding (Const)--import IRTS.Lang-import Idris.Core.TT import Idris.Core.CaseTree+import Idris.Core.TT+import IRTS.Lang++import Control.Applicative hiding (Const)+import Control.Monad.State hiding (lift) import Data.List import Debug.Trace 

@@ -8,19 +8,17 @@ {-# LANGUAGE OverloadedStrings #-} module IRTS.Portable (writePortable) where -import Data.Aeson-import qualified Data.ByteString.Lazy as B-import qualified Data.Text as T- import Idris.Core.CaseTree import Idris.Core.TT- import IRTS.Bytecode import IRTS.CodegenCommon import IRTS.Defunctionalise import IRTS.Lang import IRTS.Simplified +import Data.Aeson+import qualified Data.ByteString.Lazy as B+import qualified Data.Text as T import System.IO  data CodegenFile = CGFile {

@@ -7,13 +7,13 @@ -} module IRTS.Simplified(simplifyDefs, SDecl(..), SExp(..), SAlt(..)) where -import IRTS.Defunctionalise-import Idris.Core.TT import Idris.Core.CaseTree+import Idris.Core.TT import Idris.Core.Typecheck-import Data.Maybe-import Control.Monad.State+import IRTS.Defunctionalise +import Control.Monad.State+import Data.Maybe import Debug.Trace  data SExp = SV LVar

@@ -7,47 +7,58 @@ -} {-# LANGUAGE CPP #-} module IRTS.System( getDataFileName-                  , getDataDir-                  , getTargetDir                   , getCC                   , getLibFlags+                  , getIdrisDataDir                   , getIdrisLibDir+                  , getIdrisDocDir+                  , getIdrisCRTSDir+                  , getIdrisJSRTSDir                   , getIncFlags                   , getEnvFlags                   , version                   ) where -import Data.List.Split--import Control.Applicative ((<$>))-import Data.Maybe (fromMaybe)-import System.FilePath ((</>), addTrailingPathSeparator)-import System.Environment- #ifdef FREESTANDING-import Target_idris import Paths_idris (version)+import Target_idris #else import Paths_idris #endif -overrideDataDirWith :: String -> IO FilePath-overrideDataDirWith envVar = do-  envValue <- lookupEnv envVar+import Control.Applicative ((<$>))+import Data.List.Split+import Data.Maybe (fromMaybe)+import System.Environment+import System.FilePath (addTrailingPathSeparator, (</>))+++getIdrisDataDir :: IO String+getIdrisDataDir = do+  envValue <- lookupEnv "TARGET"   case envValue of     Nothing -> do       ddir <- getDataDir-      return (ddir </> "libs")+      return ddir     Just ddir -> return ddir +overrideIdrisSubDirWith :: String  -- ^ Sub directory in `getDataDir` location.+                        -> String  -- ^ Environment variable to get new location from.+                        -> IO FilePath+overrideIdrisSubDirWith fp envVar = do+  envValue <- lookupEnv envVar+  case envValue of+    Nothing -> do+      ddir <- getIdrisDataDir+      return (ddir </> fp)+    Just ddir -> return ddir+ getCC :: IO String getCC = fromMaybe "gcc" <$> lookupEnv "IDRIS_CC"  getEnvFlags :: IO [String] getEnvFlags = maybe [] (splitOn " ") <$> lookupEnv "IDRIS_CFLAGS" -getTargetDir :: IO String-getTargetDir = overrideDataDirWith "TARGET"  #if defined(freebsd_HOST_OS) || defined(dragonfly_HOST_OS)\     || defined(openbsd_HOST_OS) || defined(netbsd_HOST_OS)@@ -64,11 +75,21 @@ gmpLib = [] #endif -getLibFlags = do dir <- getDataDir-                 return $ ["-L" ++ (dir </> "rts"),+getLibFlags = do dir <- getIdrisCRTSDir+                 return $ ["-L" ++ dir,                            "-lidris_rts"] ++ extraLib ++ gmpLib ++ ["-lpthread"] -getIdrisLibDir = addTrailingPathSeparator <$> overrideDataDirWith "IDRIS_LIBRARY_PATH"+getIdrisLibDir = addTrailingPathSeparator <$> overrideIdrisSubDirWith "libs" "IDRIS_LIBRARY_PATH" -getIncFlags = do dir <- getDataDir-                 return $ ("-I" ++ dir </> "rts") : extraInclude+getIdrisDocDir = addTrailingPathSeparator <$> overrideIdrisSubDirWith "docs" "IDRIS_DOC_PATH"++getIdrisJSRTSDir = do+  ddir <- getIdrisDataDir+  return $ addTrailingPathSeparator (ddir </> "jsrts")++getIdrisCRTSDir = do+  ddir <- getIdrisDataDir+  return $ addTrailingPathSeparator (ddir </> "rts")++getIncFlags = do dir <- getIdrisCRTSDir+                 return $ ("-I" ++ dir) : extraInclude

@@ -41,19 +41,20 @@     Field(), cg_usedpos, ctxt_lookup, fgetState, fmodifyState   , fputState, idris_fixities, ist_callgraph, ist_optimisation   , known_interfaces, known_terms, opt_detaggable, opt_inaccessible-  , opts_idrisCmdline, repl_definitions+  , opt_forceable, opts_idrisCmdline, repl_definitions   ) where -import Control.Category+import Idris.AbsSyntaxTree+import Idris.Core.Evaluate+import Idris.Core.TT++import Prelude hiding (id, (.))+ import Control.Applicative+import Control.Category import Control.Monad.State.Class import Data.Maybe-import Prelude hiding (id, (.)) -import Idris.Core.TT-import Idris.Core.Evaluate-import Idris.AbsSyntaxTree- data Field rec fld = Field     { fget :: rec -> fld     , fset :: fld -> rec -> rec@@ -110,6 +111,7 @@       maybe_default Optimise         { inaccessible = []         , detaggable = False+        , forceable = []         }     . ctxt_lookup n     . Field idris_optimisation (\v ist -> ist{ idris_optimisation = v })@@ -121,12 +123,14 @@ opt_detaggable :: Field OptInfo Bool opt_detaggable = Field detaggable (\v opt -> opt{ detaggable = v }) +opt_forceable :: Field OptInfo [Int]+opt_forceable = Field forceable (\v opt -> opt{ forceable = v })  -- | callgraph record for the given (exact) name ist_callgraph :: Name -> Field IState CGInfo ist_callgraph n =       maybe_default CGInfo-        { calls = [], scg = [], usedpos = []+        { calls = [], allCalls = Nothing, scg = [], usedpos = []         }     . ctxt_lookup n     . Field idris_callgraph (\v ist -> ist{ idris_callgraph = v })

@@ -5,53 +5,47 @@ License     : BSD3 Maintainer  : The Idris Community. -}-{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,-             TypeSynonymInstances, PatternGuards #-}+{-# LANGUAGE DeriveFunctor, FlexibleInstances, MultiParamTypeClasses,+             PatternGuards, TypeSynonymInstances #-}  module Idris.AbsSyntax(     module Idris.AbsSyntax   , module Idris.AbsSyntaxTree   ) where -import Idris.Core.TT-import Idris.Core.Evaluate-import Idris.Core.Elaborate hiding (Tactic(..))-import Idris.Core.Typecheck import Idris.AbsSyntaxTree import Idris.Colours+import Idris.Core.Elaborate hiding (Tactic(..))+import Idris.Core.Evaluate+import Idris.Core.TT+import Idris.Core.Typecheck import Idris.Docstrings import Idris.IdeMode hiding (Opt(..)) import IRTS.CodegenCommon-import Util.DynamicLinker -import System.Console.Haskeline-import System.IO-import System.Directory (canonicalizePath, doesFileExist)+import Util.DynamicLinker+import Util.Pretty+import Util.ScreenSize+import Util.System  import Control.Applicative import Control.Monad (liftM3) import Control.Monad.State--import Data.List hiding (insert,union) import Data.Char-import qualified Data.Text as T import Data.Either+import Data.Generics.Uniplate.Data (descend, descendM)+import Data.List hiding (insert, union) import qualified Data.Map as M import Data.Maybe import qualified Data.Set as S+import qualified Data.Text as T import Data.Word (Word)--import Data.Generics.Uniplate.Data (descend, descendM)- import Debug.Trace--import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)- import Network (PortID(PortNumber))--import Util.Pretty-import Util.ScreenSize-import Util.System+import System.Console.Haskeline+import System.Directory (canonicalizePath, doesFileExist)+import System.IO+import System.IO.Error (ioeGetErrorString, isUserError, tryIOError)  getContext :: Idris Context getContext = do i <- getIState; return (tt_ctxt i)@@ -214,6 +208,13 @@ setFlags :: Name -> [FnOpt] -> Idris () setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) } +addFnOpt :: Name -> FnOpt -> Idris ()+addFnOpt n f = do i <- getIState+                  let fls = case lookupCtxtExact n (idris_flags i) of+                                 Nothing -> []+                                 Just x -> x+                  setFlags n (f : fls)+ setFnInfo :: Name -> FnInfo -> Idris () setFnInfo n fs = do i <- getIState; putIState $ i { idris_fninfo = addDef n fs (idris_fninfo i) } @@ -270,9 +271,9 @@ addCalls n calls    = do i <- getIState         case lookupCtxtExact n (idris_callgraph i) of-             Nothing -> addToCG n (CGInfo calls [] [])-             Just (CGInfo cs scg used) ->-                addToCG n (CGInfo (nub (calls ++ cs)) scg used)+             Nothing -> addToCG n (CGInfo calls Nothing [] [])+             Just (CGInfo cs ans scg used) ->+                addToCG n (CGInfo (nub (calls ++ cs)) ans scg used)  addTyInferred :: Name -> Idris () addTyInferred n@@ -364,15 +365,36 @@  -- | Trace all the names in a call graph starting at the given name getAllNames :: Name -> Idris [Name]-getAllNames n = allNames [] n+getAllNames n = do i <- getIState+                   case getCGAllNames i n of+                        Just ns -> return ns+                        Nothing -> do ns <- allNames [] n+                                      addCGAllNames i n ns+                                      return ns +getCGAllNames :: IState -> Name -> Maybe [Name]+getCGAllNames i n = case lookupCtxtExact n (idris_callgraph i) of+                         Just ci -> allCalls ci+                         _ -> Nothing++addCGAllNames :: IState -> Name -> [Name] -> Idris ()+addCGAllNames i n ns+      = case lookupCtxtExact n (idris_callgraph i) of+             Just ci -> addToCG n (ci { allCalls = Just ns })+             _ -> addToCG n (CGInfo [] (Just ns) [] [])+ allNames :: [Name] -> Name -> Idris [Name] allNames ns n | n `elem` ns = return [] allNames ns n = do i <- getIState-                   case lookupCtxtExact n (idris_callgraph i) of-                      Just ns' -> do more <- mapM (allNames (n:ns)) (calls ns')-                                     return (nub (n : concat more))-                      _ -> return [n]+                   case getCGAllNames i n of+                        Just ns -> return ns+                        Nothing -> case lookupCtxtExact n (idris_callgraph i) of+                                        Just ci -> +                                          do more <- mapM (allNames (n:ns)) (calls ci)+                                             let ns' = nub (n : concat more)+                                             addCGAllNames i n ns'+                                             return ns'+                                        _ -> return [n]  addCoercion :: Name -> Idris () addCoercion n = do i <- getIState@@ -450,10 +472,10 @@ addImplementation int res n i     = do ist <- getIState          case lookupCtxt n (idris_interfaces ist) of-                [CI a b c d e ins fds] ->-                     do let cs = addDef n (CI a b c d e (addI i ins) fds) (idris_interfaces ist)+                [CI a b c d e f g ins fds] ->+                     do let cs = addDef n (CI a b c d e f g (addI i ins) fds) (idris_interfaces ist)                         putIState $ ist { idris_interfaces = cs }-                _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [(i, res)] []) (idris_interfaces ist)+                _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [] [] [(i, res)] []) (idris_interfaces ist)                         putIState $ ist { idris_interfaces = cs }   where addI, insI :: Name -> [(Name, Bool)] -> [(Name, Bool)]         addI i ins | int = (i, res) : ins@@ -668,9 +690,9 @@    where pErase (CaseOp c t tys orig tot cds)             = CaseOp c t tys orig [] (pErase' cds)          pErase x = x-         pErase' (CaseDefs _ (cs, c) _ rs)+         pErase' (CaseDefs (cs, c) rs)              = let c' = (cs, fmap pEraseType c) in-                   CaseDefs c' c' c' rs+                   CaseDefs c' rs  checkUndefined :: FC -> Name -> Idris () checkUndefined fc n@@ -2545,7 +2567,7 @@ getPkgDir _ = Nothing  getPkg :: Opt -> Maybe (Bool, String)-getPkg (PkgBuild str) = Just (False, str)+getPkg (PkgBuild   str) = Just (False, str) getPkg (PkgInstall str) = Just (True, str) getPkg _ = Nothing @@ -2563,9 +2585,10 @@  -- | Returns None if given an Opt which is not PkgMkDoc --   Otherwise returns Just x, where x is the contents of PkgMkDoc-getPkgMkDoc :: Opt          -- ^ Opt to extract-            -> Maybe String -- ^ Result-getPkgMkDoc (PkgMkDoc str) = Just str+getPkgMkDoc :: Opt                  -- ^ Opt to extract+            -> Maybe (Bool, String) -- ^ Result+getPkgMkDoc (PkgDocBuild  str)  = Just (False,str)+getPkgMkDoc (PkgDocInstall str) = Just (True,str) getPkgMkDoc _              = Nothing  getPkgTest :: Opt          -- ^ the option to extract

@@ -5,54 +5,48 @@ License     : BSD3 Maintainer  : The Idris Community. -}-{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,-             DeriveDataTypeable, DeriveGeneric, TypeSynonymInstances,-             PatternGuards #-}+{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveGeneric,+             FlexibleInstances, MultiParamTypeClasses, PatternGuards,+             TypeSynonymInstances #-}  module Idris.AbsSyntaxTree where -import Idris.Core.TT-import Idris.Core.Evaluate+import Idris.Colours import Idris.Core.Elaborate hiding (Tactic(..))+import Idris.Core.Evaluate+import Idris.Core.TT import Idris.Core.Typecheck import Idris.Docstrings-import IRTS.Lang import IRTS.CodegenCommon-import Util.Pretty+import IRTS.Lang import Util.DynamicLinker--import Idris.Colours--import System.Console.Haskeline-import System.IO+import Util.Pretty  import Prelude hiding ((<$>))  import Control.Applicative ((<|>))--import Control.Monad.Trans.State.Strict-import Control.Monad.Trans.Except import qualified Control.Monad.Trans.Class as Trans (lift)-+import Control.Monad.Trans.Except+import Control.Monad.Trans.State.Strict+import Data.Char import Data.Data (Data)+import Data.Either+import Data.Foldable (Foldable) import Data.Function (on)-import Data.Generics.Uniplate.Data (universe, children)+import Data.Generics.Uniplate.Data (children, universe) import Data.List hiding (group)-import Data.Char import qualified Data.Map.Strict as M-import qualified Data.Text as T-import Data.Either-import qualified Data.Set as S-import Data.Word (Word) import Data.Maybe (fromMaybe, mapMaybe, maybeToList)+import qualified Data.Set as S+import qualified Data.Text as T import Data.Traversable (Traversable) import Data.Typeable-import Data.Foldable (Foldable)-import GHC.Generics (Generic)-import Network.Socket(PortNumber)-+import Data.Word (Word) import Debug.Trace-+import GHC.Generics (Generic)+import Network.Socket (PortNumber)+import System.Console.Haskeline+import System.IO import Text.PrettyPrint.Annotated.Leijen  data ElabWhat = ETypes | EDefns | EAll@@ -327,9 +321,10 @@ type UsageReason = (Name, Int)  -- fn_name, its_arg_number  data CGInfo = CGInfo {-    calls   :: [Name]-  , scg     :: [SCGEntry]-  , usedpos :: [(Int, [UsageReason])]+    calls    :: [Name] -- Immediate calls+  , allCalls :: Maybe [Name] -- Calls and descendents (built as required, for PE)+  , scg      :: [SCGEntry]+  , usedpos  :: [(Int, [UsageReason])]   } deriving (Show, Generic) {-! deriving instance Binary CGInfo@@ -367,7 +362,7 @@               | IBCMetaInformation Name MetaInformation               | IBCTotal Name Totality               | IBCInjective Name Injectivity-              | IBCFlags Name [FnOpt]+              | IBCFlags Name               | IBCFnInfo Name FnInfo               | IBCTrans Name (Term, Term)               | IBCErrRev (Term, Term)@@ -492,7 +487,8 @@          | IdemodeSocket          | ShowAll          | ShowLibs-         | ShowLibdir+         | ShowLibDir+         | ShowDocDir          | ShowIncs          | ShowPkgs          | ShowLoggingCats@@ -524,7 +520,8 @@          | PkgClean String          | PkgCheck String          | PkgREPL String-         | PkgMkDoc String -- IdrisDoc+         | PkgDocBuild String -- IdrisDoc+         | PkgDocInstall String          | PkgTest String          | PkgIndex FilePath          | WarnOnly@@ -589,7 +586,7 @@   data Static = Static | Dynamic-  deriving (Show, Eq, Data, Generic, Typeable)+  deriving (Show, Eq, Ord, Data, Generic, Typeable) {-! deriving instance Binary Static !-}@@ -612,7 +609,7 @@                       , pstatic  :: Static                       , pscript  :: PTerm                       }-             deriving (Show, Eq, Data, Generic, Typeable)+             deriving (Show, Eq, Ord, Data, Generic, Typeable)  {-! deriving instance Binary Plicity@@ -640,11 +637,13 @@  data FnOpt = Inlinable -- ^ always evaluate when simplifying            | TotalFn | PartialFn | CoveringFn-           | Coinductive | AssertTotal+           | AllGuarded -- ^ all delayed arguments guaranteed guarded by constructors+           | AssertTotal             -- | interface dictionary, eval only when a function            -- argument, and further evaluation results.            | Dictionary+           | OverlappingDictionary -- ^ Interface dictionary which may overlap            | Implicit                       -- ^ implicit coercion            | NoImplicit                     -- ^ do not apply implicit coercions            | CExport String                 -- ^ export, with a C name@@ -652,6 +651,12 @@            | ErrorReverse                   -- ^ attempt to reverse normalise before showing in error            | Reflection                     -- ^ a reflecting function, compile-time only            | Specialise [(Name, Maybe Int)] -- ^ specialise it, freeze these names+           | UnfoldIface Name [Name]+                  -- ^ Unfold given interface name in the definition, the+                  -- top level methods, and anything which has+                  -- the interface name as an argument. This is to unfold+                  -- things for termination checking, as interfaces will otherwise+                  -- cause problems            | Constructor -- ^ Data constructor type            | AutoHint    -- ^ use in auto implicit search            | PEGenerated -- ^ generated by partial evaluator@@ -1035,7 +1040,7 @@ data PunInfo = IsType              | IsTerm              | TypeOrTerm-             deriving (Eq, Show, Data, Typeable, Generic)+             deriving (Eq, Show, Ord, Data, Typeable, Generic)  -- | High level language terms data PTerm = PQuote Raw         -- ^ Inclusion of a core term into the@@ -1101,12 +1106,12 @@            | PConstSugar FC PTerm              -- ^ A desugared constant. The FC is a precise source              -- location that will be used to highlight it later.-       deriving (Eq, Data, Typeable, Generic)+       deriving (Eq, Ord, Data, Typeable, Generic)  data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed               | FirstSuccess               | TryImplicit-       deriving (Eq, Data, Generic, Typeable)+       deriving (Eq, Ord, Data, Generic, Typeable)  -- | Transform the FCs in a PTerm. The first function transforms the -- general-purpose FCs, and the second transforms those that are used@@ -1225,7 +1230,7 @@                 | TFail [ErrorReportPart]                 | Qed | Abandon                 | SourceFC-    deriving (Show, Eq, Functor, Foldable, Traversable, Data, Generic, Typeable)+    deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Data, Generic, Typeable) {-! deriving instance Binary PTactic' !-}@@ -1271,7 +1276,7 @@             | DoBindP FC t t [(t,t)]             | DoLet  FC Name FC t t   -- ^ second FC is precise name location             | DoLetP FC t t-    deriving (Eq, Functor, Data, Generic, Typeable)+    deriving (Eq, Ord, Functor, Data, Generic, Typeable) {-! deriving instance Binary PDo' !-}@@ -1311,13 +1316,13 @@                             , getScript :: t                             , getTm     :: t                             }-             deriving (Show, Eq, Functor, Data, Generic, Typeable)+             deriving (Show, Eq, Ord, Functor, Data, Generic, Typeable)  data ArgOpt = AlwaysShow             | HideDisplay             | InaccessibleArg             | UnknownImp-            deriving (Show, Eq, Data, Generic, Typeable)+            deriving (Show, Eq, Ord, Data, Generic, Typeable)  instance Sized a => Sized (PArg' a) where   size (PImp p _ l nm trm)            = 1 + size nm + size trm@@ -1402,7 +1407,9 @@   , interface_methods                  :: [(Name, (Bool, FnOpts, PTerm))] -- ^ flag whether it's a "data" method   , interface_defaults                 :: [(Name, (Name, PDecl))]         -- ^ method name -> default impl   , interface_default_super_interfaces :: [PDecl]+  , interface_impparams                :: [Name]   , interface_params                   :: [Name]+  , interface_constraints              :: [PTerm]   , interface_implementations          :: [(Name, Bool)] -- ^ the Bool is whether to include in implementation search, so named implementations are excluded   , interface_determiners              :: [Int]   } deriving (Show, Generic)@@ -1433,6 +1440,7 @@ data OptInfo = Optimise {     inaccessible :: [(Int,Name)]  -- includes names for error reporting   , detaggable :: Bool+  , forceable :: [Int] -- argument positions which are forced by other values   } deriving (Show, Generic) {-! deriving instance Binary OptInfo@@ -1789,9 +1797,18 @@       | Just n <- snat ppo d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))     prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n     prettySe d p bnd (PLam fc n nfc ty sc) =-      depth d . bracket p startPrec . group . align . hang 2 $-      text "\\" <> prettyBindingOf n False <+> text "=>" <$>-      prettySe (decD d) startPrec ((n, False):bnd) sc+      let (ns, sc') = getLamNames [n] sc in+          depth d . bracket p startPrec . group . align . hang 2 $+          text "\\" <> prettyBindingsOf ns False <+> text "=>" <$>+          prettySe (decD d) startPrec ((n, False):bnd) sc'+      where+        getLamNames acc (PLam fc n nfc ty sc) = getLamNames (n : acc) sc+        getLamNames acc sc = (reverse acc, sc)++        prettyBindingsOf [] t = text ""+        prettyBindingsOf [n] t = prettyBindingOf n t+        prettyBindingsOf (n : ns) t = prettyBindingOf n t <> text "," <+>+                                      prettyBindingsOf ns t     prettySe d p bnd (PLet fc n nfc ty v sc) =       depth d . bracket p startPrec . group . align $       kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>@@ -2548,5 +2565,5 @@ getErasureInfo :: IState -> Name -> [Int] getErasureInfo ist n =     case lookupCtxtExact n (idris_optimisation ist) of-        Just (Optimise inacc detagg) -> map fst inacc+        Just (Optimise inacc detag force) -> map fst inacc         Nothing -> []

@@ -8,12 +8,12 @@ module Idris.Apropos (apropos, aproposModules) where  import Idris.AbsSyntax-import Idris.Core.Evaluate (ctxtAlist, Def(..))-import Idris.Core.TT (Name(..), Type, TT(..), NameType(..), Binder(..), Const(..),-                      lookupCtxtExact, toAlist)-import Idris.Docstrings (Docstring, DocTerm, containsText)+import Idris.Core.Evaluate (Def(..), ctxtAlist)+import Idris.Core.TT (Binder(..), Const(..), Name(..), NameType(..), TT(..),+                      Type, lookupCtxtExact, toAlist)+import Idris.Docstrings (DocTerm, Docstring, containsText) -import Data.List (nub, nubBy, intersperse)+import Data.List (intersperse, nub, nubBy) import qualified Data.Text as T  -- | Find definitions that are relevant to all space-delimited components of

@@ -28,33 +28,29 @@   ) where  import Idris.AbsSyntax-import Idris.AbsSyntaxTree (Idris, IState, PTerm)-import Idris.ElabDecls+import Idris.AbsSyntaxTree (IState, Idris, PTerm)+import Idris.Core.Evaluate+import Idris.Core.TT+import Idris.Core.Typecheck import Idris.Delaborate-import Idris.Parser-import Idris.Parser.Helpers+import Idris.Elab.Term+import Idris.Elab.Value+import Idris.ElabDecls import Idris.Error import Idris.Output--import Idris.Elab.Value-import Idris.Elab.Term--import Idris.Core.TT-import Idris.Core.Typecheck-import Idris.Core.Evaluate+import Idris.Parser+import Idris.Parser.Helpers -import Data.Maybe-import Data.Char-import Data.List (isPrefixOf, isSuffixOf) import Control.Monad import Control.Monad.State.Strict-+import Data.Char+import Data.List (isPrefixOf, isSuffixOf)+import Data.Maybe+import Debug.Trace+import Text.Parser.Char (anyChar) import Text.Parser.Combinators-import Text.Parser.Char(anyChar)-import Text.Trifecta(Result(..), parseString)+import Text.Trifecta (Result(..), parseString) import Text.Trifecta.Delta--import Debug.Trace  -- | Given a variable to split, and a term application, return a list -- of variable updates, paired with a flag to say whether the given

@@ -11,22 +11,21 @@   , ModuleTree(..)   ) where -import Idris.Core.TT-import Idris.Parser import Idris.AbsSyntax-import Idris.Imports-import Idris.Unlit+import Idris.Core.TT import Idris.Error import Idris.IBC+import Idris.Imports+import Idris.Parser+import Idris.Unlit -import System.FilePath-import System.Directory-import Data.Time.Clock-import Control.Monad.Trans import Control.Monad.State+import Control.Monad.Trans import Data.List-+import Data.Time.Clock import Debug.Trace+import System.Directory+import System.FilePath import Util.System (readSource, writeSource)  data ModuleTree = MTree { mod_path :: IFileType,

@@ -1,3 +1,4 @@+{-# LANGUAGE CPP #-} {-| Module      : Idris.CmdOptions Description : A parser for the CmdOptions for the Idris executable.@@ -13,27 +14,27 @@   , getPkgREPL, getPkgTest, getPort, getIBCSubDir   ) where +import Idris.AbsSyntax (getClient, getIBCSubDir, getPkg, getPkgCheck,+                        getPkgClean, getPkgMkDoc, getPkgREPL, getPkgTest,+                        getPort, opt) import Idris.AbsSyntaxTree-import Idris.AbsSyntax (opt, getClient, getPkg, getPkgCheck, getPkgClean, getPkgMkDoc-  , getPkgREPL, getPkgTest, getPort, getIBCSubDir)--- import Idris.REPL import Idris.Info (getIdrisVersion)-+-- import Idris.REPL import IRTS.CodegenCommon -import Options.Applicative-import Options.Applicative.Arrows-import Options.Applicative.Types (ReadM(..)) import Control.Monad.Trans (lift)-import Control.Monad.Trans.Reader (ask) import Control.Monad.Trans.Except (throwE)+import Control.Monad.Trans.Reader (ask) import Data.Char import Data.Maybe--import Text.ParserCombinators.ReadP hiding (many, option)-+#if MIN_VERSION_optparse_applicative(0,13,0)+import Data.Monoid ((<>))+#endif+import Options.Applicative+import Options.Applicative.Arrows+import Options.Applicative.Types (ReadM(..)) import Safe (lastMay)-+import Text.ParserCombinators.ReadP hiding (many, option) import qualified Text.PrettyPrint.ANSI.Leijen as PP  runArgParser :: IO [Opt]@@ -129,7 +130,8 @@   <|> flag' ShowLoggingCats (long "listlogcats" <> help "Display logging categories")   <|> flag' ShowLibs        (long "link"        <> help "Display link flags")   <|> flag' ShowPkgs        (long "listlibs"    <> help "Display installed libraries")-  <|> flag' ShowLibdir      (long "libdir"      <> help "Display library directory")+  <|> flag' ShowLibDir      (long "libdir"      <> help "Display library directory")+  <|> flag' ShowDocDir      (long "docdir"      <> help "Display idrisdoc install directory")   <|> flag' ShowIncs        (long "include"     <> help "Display the includes flags")    <|> flag' Verbose (short 'V' <> long "verbose" <> help "Loud verbosity")@@ -144,13 +146,14 @@   <|> (Port <$> option portReader (long "port" <> metavar "PORT" <> help "REPL TCP port - pass \"none\" to not bind any port"))    -- Package commands-  <|> (PkgBuild   <$> strOption (long "build"    <> metavar "IPKG" <> help "Build package"))-  <|> (PkgInstall <$> strOption (long "install"  <> metavar "IPKG" <> help "Install package"))-  <|> (PkgREPL    <$> strOption (long "repl"     <> metavar "IPKG" <> help "Launch REPL, only for executables"))-  <|> (PkgClean   <$> strOption (long "clean"    <> metavar "IPKG" <> help "Clean package"))-  <|> (PkgMkDoc   <$> strOption (long "mkdoc"    <> metavar "IPKG" <> help "Generate IdrisDoc for package"))-  <|> (PkgCheck   <$> strOption (long "checkpkg" <> metavar "IPKG" <> help "Check package only"))-  <|> (PkgTest    <$> strOption (long "testpkg"  <> metavar "IPKG" <> help "Run tests for package"))+  <|> (PkgBuild      <$> strOption (long "build"      <> metavar "IPKG" <> help "Build package"))+  <|> (PkgInstall    <$> strOption (long "install"    <> metavar "IPKG" <> help "Install package"))+  <|> (PkgREPL       <$> strOption (long "repl"       <> metavar "IPKG" <> help "Launch REPL, only for executables"))+  <|> (PkgClean      <$> strOption (long "clean"      <> metavar "IPKG" <> help "Clean package"))+  <|> (PkgDocBuild   <$> strOption (long "mkdoc"      <> metavar "IPKG" <> help "Generate IdrisDoc for package"))+  <|> (PkgDocInstall <$> strOption (long "installdoc" <> metavar "IPKG" <> help "Install IdrisDoc for package"))+  <|> (PkgCheck      <$> strOption (long "checkpkg"   <> metavar "IPKG" <> help "Check package only"))+  <|> (PkgTest       <$> strOption (long "testpkg"    <> metavar "IPKG" <> help "Run tests for package"))    -- Misc options   <|> (BCAsm <$> strOption (long "bytecode"))

@@ -7,28 +7,26 @@ -} module Idris.Completion (replCompletion, proverCompletion) where -import Idris.Core.Evaluate (definitions, ctxtAlist)-import Idris.Core.TT- import Idris.AbsSyntax (runIO) import Idris.AbsSyntaxTree+import Idris.Colours+import Idris.Core.Evaluate (ctxtAlist, definitions)+import Idris.Core.TT import Idris.Help import Idris.Imports (installedPackages)-import Idris.Colours-import Idris.Parser.Helpers(opChars)+import Idris.Parser.Expr (TacticArg(..)) import qualified Idris.Parser.Expr (constants, tactics)-import Idris.Parser.Expr (TacticArg (..))+import Idris.Parser.Helpers (opChars) import Idris.REPL.Parser (allHelp, setOptions)-import Control.Monad.State.Strict +import Control.Monad.State.Strict+import Data.Char (toLower) import Data.List-import Data.Maybe-import Data.Char(toLower) import qualified Data.Map.Strict as Map+import Data.Maybe import qualified Data.Text as T--import System.Console.Haskeline import System.Console.ANSI (Color)+import System.Console.Haskeline  commands = [ n | (names, _, _) <- allHelp ++ extraHelp, n <- names ] 

@@ -8,15 +8,15 @@ {-# OPTIONS_GHC -fwarn-incomplete-patterns #-} module Idris.Core.Binary where -import Control.Applicative ((<*>), (<$>))-import Control.Monad (liftM2)-import Control.DeepSeq (($!!))+import Idris.Core.TT +import Control.Applicative ((<$>), (<*>))+import Control.DeepSeq (($!!))+import Control.Monad (liftM2) import Data.Binary-import Data.Vector.Binary import qualified Data.Text as T import qualified Data.Text.Encoding as E-import Idris.Core.TT+import Data.Vector.Binary  instance Binary ErrorReportPart where   put (TextPart msg) = do putWord8 0 ; put msg@@ -639,6 +639,7 @@                 TType x1 -> do putWord8 7                                put x1                 Impossible -> putWord8 8+                Inferred x1 -> put x1 -- drop the 'Inferred'                 UType x1 -> do putWord8 10                                put x1         get

@@ -18,8 +18,8 @@ in order to allow for better optimisation opportunities.  -}-{-# LANGUAGE PatternGuards, DeriveFunctor, TypeSynonymInstances,-    DeriveGeneric #-}+{-# LANGUAGE DeriveFunctor, DeriveGeneric, PatternGuards, TypeSynonymInstances+             #-}  module Idris.Core.CaseTree (     CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..), ErasureInfo@@ -31,11 +31,12 @@ import Idris.Core.TT  import Control.Applicative hiding (Const)-import Control.Monad.State import Control.Monad.Reader-import Data.Maybe+import Control.Monad.State import Data.List hiding (partition)-import qualified Data.List(partition)+import qualified Data.List (partition)+import Data.Maybe+import qualified Data.Set as S import Debug.Trace import GHC.Generics (Generic) @@ -153,33 +154,34 @@ findCalls = findCalls' False  findCalls' :: Bool -> SC -> [Name] -> [(Name, [[Name]])]-findCalls' ignoreasserts sc topargs = nub $ nu' topargs sc where-    nu' ps (Case _ n alts) = nub (concatMap (nua (n : ps)) alts)-    nu' ps (ProjCase t alts) = nub $ nut ps t ++ concatMap (nua ps) alts-    nu' ps (STerm t)     = nub $ nut ps t-    nu' ps _ = []+findCalls' ignoreasserts sc topargs = S.toList $ nu' topargs sc where+    nu' ps (Case _ n alts) = S.unions $ map (nua (n : ps)) alts+    nu' ps (ProjCase t alts) = S.unions $ nut ps t : map (nua ps) alts+    nu' ps (STerm t)     = nut ps t+    nu' ps _ = S.empty -    nua ps (ConCase n i args sc) = nub (nu' (ps ++ args) sc)-    nua ps (FnCase n args sc) = nub (nu' (ps ++ args) sc)+    nua ps (ConCase n i args sc) = nu' (ps ++ args) sc+    nua ps (FnCase n args sc) = nu' (ps ++ args) sc     nua ps (ConstCase _ sc) = nu' ps sc     nua ps (SucCase _ sc) = nu' ps sc     nua ps (DefaultCase sc) = nu' ps sc -    nut ps (P _ n _) | n `elem` ps = []-                     | otherwise = [(n, [])] -- tmp+    nut ps (P _ n _) | n `elem` ps = S.empty+                     | otherwise = S.singleton (n, [])     nut ps fn@(App _ f a)         | (P _ n _, args) <- unApply fn-             = if ignoreasserts && n == sUN "assert_total" -                  then []-                  else if n `elem` ps -                          then nut ps f ++ nut ps a-                          else [(n, map argNames args)] ++ concatMap (nut ps) args-        | (P (TCon _ _) n _, _) <- unApply fn = []-        | otherwise = nut ps f ++ nut ps a-    nut ps (Bind n (Let t v) sc) = nut ps v ++ nut (n:ps) sc+             = if ignoreasserts && n == sUN "assert_total"+                  then S.empty+                  else if n `elem` ps+                          then S.union (nut ps f) (nut ps a)+                          else S.insert (n, map argNames args) +                                   (S.unions $ map (nut ps) args)+        | (P (TCon _ _) n _, _) <- unApply fn = S.empty+        | otherwise = S.union (nut ps f) (nut ps a)+    nut ps (Bind n (Let t v) sc) = S.union (nut ps v) (nut (n:ps) sc)     nut ps (Proj t _) = nut ps t     nut ps (Bind n b sc) = nut (n:ps) sc-    nut ps _ = []+    nut ps _ = S.empty      argNames tm = let ns = directUse tm in                       filter (\x -> x `elem` ns) topargs@@ -242,14 +244,18 @@ runCaseBuilder :: ErasureInfo -> CaseBuilder a -> (CS -> (a, CS)) runCaseBuilder ei bld = runState $ runReaderT bld ei -data Phase = CompileTime | RunTime+data Phase = CoverageCheck [Int] -- list of positions explicitly given+           | CompileTime +           | RunTime     deriving (Show, Eq)  -- Generate a simple case tree -- Work Right to Left  simpleCase :: Bool -> SC -> Bool ->-              Phase -> FC -> [Int] -> +              Phase -> FC -> +              -- Following two can be empty lists when Phase = CoverageCheck+              [Int] -> -- Inaccessible argument positions               [(Type, Bool)] -> -- (Argument type, whether it's canonical)               [([Name], Term, Term)] ->               ErasureInfo ->@@ -289,7 +295,7 @@           -- Check that all pattern variables are reachable by a case split           -- Otherwise, they won't make sense on the RHS.           chkAccessible (avs, l, c)-               | phase == RunTime || reflect = return (l, c)+               | phase /= CompileTime || reflect = return (l, c)                | otherwise = do mapM_ (acc l) avs                                 return (l, c) @@ -343,6 +349,7 @@  data Pat = PCon Bool Name Int [Pat]          | PConst Const+         | PInferred Pat          | PV Name Type          | PSuc Pat -- special case for n+1 on Integer          | PReflected Name [Pat]@@ -381,6 +388,7 @@      toPat' []   (P Bound n ty) = PV n ty     toPat' args (App _ f a)    = toPat' (a : args) f+    toPat' args (Inferred tm)  = PInferred (toPat' args tm)     toPat' [] (Constant x) | isTypeConst x = PTyPat                            | otherwise     = PConst x @@ -431,12 +439,26 @@ -- The first argument means [(Name, IsInaccessible)].  order :: Phase -> [(Name, Bool)] -> [Clause] -> [Bool] -> ([Name], [Clause])--- do nothing at compile time: FIXME (EB): Put this in after checking +-- do nothing at compile time: FIXME (EB): Put this in after checking -- implications for Franck's reflection work... see issue 3233--- order CompileTime ns cs _ = (map fst ns, cs) +-- order CompileTime ns cs _ = (map fst ns, cs) order _ []  cs cans = ([], cs) order _ ns' [] cans = (map fst ns', [])-order phase ns' cs cans +order (CoverageCheck pos) ns' cs cans +    = let ns_out = pick 0 [] (map fst ns')+          cs_out = map pickClause cs in+          (ns_out, cs_out)+  where+    pickClause (pats, def) = (pick 0 [] pats, def)++    -- Order the list so that things in a position in 'pos' are in the first+    -- part, then all the other things later. Otherwise preserve order.+    pick i skipped [] = reverse skipped+    pick i skipped (x : xs) +         | i `elem` pos = x : pick (i + 1) skipped xs+         | otherwise    = pick (i + 1) (x : skipped) xs++order phase ns' cs cans     = let patnames = transpose (map (zip ns') (map (zip cans) (map fst cs)))           -- only sort the arguments where there is no clash in           -- constructor tags between families, the argument type is canonical,@@ -444,7 +466,7 @@           -- clash, because otherwise we can't reliable make the           -- case distinction on evaluation           (patnames_ord, patnames_rest)-                = Data.List.partition (noClash . map snd) patnames +                = Data.List.partition (noClash . map snd) patnames           patnames_ord' = case phase of                                CompileTime -> patnames_ord                                -- reversing tends to make better case trees@@ -460,7 +482,7 @@     rebuild patnames clause = (map (snd . snd) patnames, snd clause)      noClash [] = True-    noClash ((can, p) : ps) = can && not (any (clashPat p) (map snd ps)) +    noClash ((can, p) : ps) = can && not (any (clashPat p) (map snd ps))                                   && noClash ps      clashPat (PCon _ _ _ _) (PConst _) = True@@ -471,7 +493,7 @@     clashPat _ _ = False      -- this compares (+isInaccessible, -numberOfCases)-    moreDistinct xs ys +    moreDistinct xs ys         = compare (snd . fst . head $ xs, numNames [] (map snd ys))                   (snd . fst . head $ ys, numNames [] (map snd xs)) @@ -482,6 +504,41 @@     numNames xs (_ : ps) = numNames xs ps     numNames xs [] = length xs +-- Reorder the patterns in the clause so that the PInferred patterns come+-- last. Also strip 'PInferred' from the top level patterns so that we can+-- go ahead and match.+orderByInf :: [Name] -> [Clause] -> ([Name], [Clause])+orderByInf vs cs = let alwaysInf = getInf cs in+                       (selectInf alwaysInf vs,+                        map deInf (map (selectExp alwaysInf) cs))+  where+    getInf [] = []+    getInf [(pats, def)] = infPos 0 pats+    getInf ((pats, def) : cs) = infPos 0 pats `intersect` getInf cs++    selectExp :: [Int] -> Clause -> Clause+    selectExp infs (pats, def)+         = let (notInf, inf) = splitPats 0 infs [] [] pats in+               (notInf ++ inf, def)++    selectInf :: [Int] -> [a] -> [a]+    selectInf infs ns = let (notInf, inf) = splitPats 0 infs [] [] ns in+                            notInf ++ inf++    splitPats i infpos notInf inf [] = (reverse notInf, reverse inf)+    splitPats i infpos notInf inf (p : ps)+         | i `elem` infpos = splitPats (i + 1) infpos notInf (p : inf) ps+         | otherwise = splitPats (i + 1) infpos (p : notInf) inf ps++    infPos i [] = []+    infPos i (PInferred p : ps) = i : infPos (i + 1) ps+    infPos i (_ : ps) = infPos (i + 1) ps++    deInf (pats, def) = (map deInfPat pats, def)++    deInfPat (PInferred p) = p+    deInfPat p = p+ match :: [Name] -> [Clause] -> SC -- error case                             -> CaseBuilder SC match [] (([], ret) : xs) err@@ -490,8 +547,9 @@          case snd ret of             Impossible -> return ImpossibleCase             tm -> return $ STerm tm -- run out of arguments-match vs cs err = do let ps = partition cs-                     mixture vs ps err+match vs cs err = do let (vs', de_inf) = orderByInf vs cs+                         ps = partition de_inf+                     mixture vs' ps err  mixture :: [Name] -> [Partition] -> SC -> CaseBuilder SC mixture vs [] err = return err

@@ -7,12 +7,12 @@ -} module Idris.Core.Constraints ( ucheck ) where -import Idris.Core.TT ( TC(..), UExp(..), UConstraint(..), FC(..),-                       ConstraintFC(..), Err'(..) )+import Idris.Core.TT (ConstraintFC(..), Err'(..), FC(..), TC(..),+                      UConstraint(..), UExp(..))  import Control.Applicative import Control.Monad.State.Strict-import Data.List ( partition )+import Data.List (partition) import qualified Data.Map.Strict as M import qualified Data.Set as S import Debug.Trace

@@ -10,9 +10,9 @@  module Idris.Core.DeepSeq where -import Idris.Core.TT import Idris.Core.CaseTree import Idris.Core.Evaluate+import Idris.Core.TT  import Control.DeepSeq 

@@ -10,29 +10,30 @@ primitives. -} -{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, PatternGuards #-} module Idris.Core.Elaborate (     module Idris.Core.Elaborate   , module Idris.Core.ProofState   ) where +import Idris.Core.DeepSeq+import Idris.Core.Evaluate import Idris.Core.ProofState-import Idris.Core.ProofTerm(bound_in, getProofTerm, mkProofTerm, bound_in_term,-                            refocus)+import Idris.Core.ProofTerm (bound_in, bound_in_term, getProofTerm, mkProofTerm,+                             refocus) import Idris.Core.TT-import Idris.Core.Evaluate import Idris.Core.Typecheck import Idris.Core.Unify-import Idris.Core.DeepSeq+import Idris.Core.WHNF +import Util.Pretty hiding (fill)+ import Control.DeepSeq import Control.Monad.State.Strict import Data.Char import Data.List import Debug.Trace -import Util.Pretty hiding (fill)- data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))   deriving Show @@ -422,9 +423,12 @@ simplify :: Elab' aux () simplify = processTactic' Simplify -hnf_compute :: Elab' aux ()-hnf_compute = processTactic' HNF_Compute+whnf_compute :: Elab' aux ()+whnf_compute = processTactic' WHNF_Compute +whnf_compute_args :: Elab' aux ()+whnf_compute_args = processTactic' WHNF_ComputeArgs+ eval_in :: Raw -> Elab' aux () eval_in t = processTactic' (EvalIn t) @@ -575,7 +579,7 @@        -- Count arguments to check if we need to normalise the type        let usety = if argsOK (finalise ty) imps                       then finalise ty-                      else normalise ctxt env (finalise ty)+                      else whnfArgs ctxt env (finalise ty)        claims <- -- trace (show (fn, imps, ty, map fst env, normalise ctxt env (finalise ty))) $                  mkClaims usety imps [] (map fst env)        ES (p, a) s prev <- get@@ -697,7 +701,7 @@     do ty <- get_type (Var n)        ctxt <- get_context        env <- get_env-       claims <- doClaims (hnf ctxt env ty) args []+       claims <- doClaims (normalise ctxt env ty) args []        prep_fill n (map fst claims)        let eclaims = sortBy (\ (_, x) (_,y) -> priOrder x y) claims        elabClaims [] False claims@@ -745,7 +749,7 @@             = do g <- goal                  ctxt <- get_context                  env <- get_env-                 case (normalise ctxt env g) of+                 case (whnf ctxt env g) of                     Bind _ (Pi _ _ _) _ -> return ()                     _ -> do a <- getNameFrom (sMN 0 "__pargTy")                             b <- getNameFrom (sMN 0 "__pretTy")@@ -820,7 +824,7 @@        focus s; attack;        ctxt <- get_context        env <- get_env-       case normalise ctxt env fty of+       case whnf ctxt env fty of             -- if f gives a function type, unify our argument type with             -- f's expected argument type             Bind _ (Pi _ argty _) _ -> unifyGoal (forget argty)

@@ -5,13 +5,14 @@ License     : BSD3 Maintainer  : The Idris Community. -}-{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, BangPatterns,-             PatternGuards, DeriveGeneric #-}+{-# LANGUAGE BangPatterns, DeriveGeneric, FlexibleInstances,+             MultiParamTypeClasses, PatternGuards #-} {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}  module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,                 normaliseAll, normaliseBlocking, toValue, quoteTerm,-                rt_simplify, simplify, specialise, hnf, convEq, convEq',+                rt_simplify, simplify, inlineSmall,+                specialise, unfold, convEq, convEq',                 Def(..), CaseInfo(..), CaseDefs(..),                 Accessibility(..), Injectivity, Totality(..), PReason(..), MetaInformation(..),                 Context, initContext, ctxtAlist, next_tvar,@@ -19,24 +20,24 @@                 addDatatype, addCasedef, simplifyCasedef, addOperator,                 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,                 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,-                mapDefCtxt,+                mapDefCtxt, tcReducible,                 lookupTotal, lookupTotalExact, lookupInjectiveExact,-                lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, +                lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict,                 isCanonical, isDConName, canBeDConName, isTConName, isConName, isFnName,                 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,                 isUniverse) where -import Debug.Trace+import Idris.Core.CaseTree+import Idris.Core.TT+ import Control.Applicative hiding (Const)-import Control.Monad.State -- not Strict!-import qualified Data.Binary as B+import Control.Monad.State import Data.Binary hiding (get, put)+import qualified Data.Binary as B import Data.Maybe (listToMaybe)+import Debug.Trace import GHC.Generics (Generic) -import Idris.Core.TT-import Idris.Core.CaseTree- data EvalState = ES { limited :: [(Name, Int)],                       nexthole :: Int,                       blocking :: Bool }@@ -45,10 +46,10 @@ type Eval a = State EvalState a  data EvalOpt = Spec-             | HNF-             | Simplify+             | Simplify Bool -- ^ whether to expand lets or not              | AtREPL              | RunTT+             | Unfold   deriving (Show, Eq)  initEval = ES [] 0 False@@ -131,10 +132,7 @@          (tm, limited st)  -- | Like normalise, but we only reduce functions that are marked as okay to--- inline (and probably shouldn't reduce lets?)--- 20130908: now only used to reduce for totality checking. Inlining should--- be done elsewhere.-+-- inline, and lets  simplify :: Context -> Env -> TT Name -> TT Name simplify ctxt env t    = evalState (do val <- eval False ctxt [(sUN "lazy", 0),@@ -146,9 +144,18 @@                                            (sUN "prim__syntactic_eq", 0),                                            (sUN "fork", 0)]                                  (map finalEntry env) (finalise t)-                                 [Simplify]+                                 [Simplify True]                    quote 0 val) initEval +-- | Like simplify, but we only reduce functions that are marked as okay to+-- inline, and don't reduce lets +inlineSmall :: Context -> Env -> TT Name -> TT Name+inlineSmall ctxt env t+   = evalState (do val <- eval False ctxt []+                                 (map finalEntry env) (finalise t)+                                 [Simplify False]+                   quote 0 val) initEval+ -- | Simplify for run-time (i.e. basic inlining) rt_simplify :: Context -> Env -> TT Name -> TT Name rt_simplify ctxt env t@@ -162,12 +169,19 @@                                  [RunTT]                    quote 0 val) initEval --- | Reduce a term to head normal form-hnf :: Context -> Env -> TT Name -> TT Name-hnf ctxt env t-   = evalState (do val <- eval False ctxt []-                                 (map finalEntry env)-                                 (finalise t) [HNF]+-- | Unfold the given names in a term, the given number of times in a stack.+-- Preserves 'let'.+-- This is primarily to support inlining of the given names, and can also+-- help with partial evaluation by allowing a rescursive definition to be+-- unfolded once only.+-- Specifically used to unfold definitions using interfaces before going to+-- the totality checker (otherwise mutually recursive definitions in+-- implementations will not work...)+unfold :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name+unfold ctxt env ns t+   = evalState (do val <- eval False ctxt ns+                               (map finalEntry env) (finalise t)+                               [Unfold]                    quote 0 val) initEval  @@ -187,22 +201,25 @@ unbindEnv env tm = error "Impossible case occurred: couldn't unbind env."  usable :: Bool -- specialising+          -> Bool -- unfolding only           -> Int -- Reduction depth limit (when simplifying/at REPL)           -> Name -> [(Name, Int)] -> Eval (Bool, [(Name, Int)]) -- usable _ _ ns@((MN 0 "STOP", _) : _) = return (False, ns)-usable False depthlimit n [] = return (True, [])-usable True depthlimit n ns+usable False uf depthlimit n [] = return (True, [])+usable True uf depthlimit n ns   = do ES ls num b <- get        if b then return (False, ns)             else case lookup n ls of                     Just 0 -> return (False, ns)                     Just i -> return (True, ns)                     _ -> return (False, ns)-usable False depthlimit n ns+usable False uf depthlimit n ns   = case lookup n ns of          Just 0 -> return (False, ns)          Just i -> return $ (True, (n, abs (i-1)) : filter (\ (n', _) -> n/=n') ns)-         _ -> return $ (True, (n, depthlimit) : filter (\ (n', _) -> n/=n') ns)+         _ -> return $ if uf +                          then (False, ns)+                          else (True, (n, depthlimit) : filter (\ (n', _) -> n/=n') ns)   fnCount :: Int -> Name -> Eval ()@@ -231,10 +248,11 @@         [EvalOpt] -> Eval Value eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where     spec = Spec `elem` opts-    simpl = Simplify `elem` opts+    simpl = Simplify True `elem` opts || Simplify False `elem` opts+    simpl_inline = Simplify False `elem` opts     runtime = RunTT `elem` opts     atRepl = AtREPL `elem` opts-    hnf = HNF `elem` opts+    unfold = Unfold `elem` opts      -- returns 'True' if the function should block     -- normal evaluation should return false@@ -243,33 +261,33 @@            = if always then False                        else not (inl || dict) || elem n stk        | simpl-           = (not (inl || dict) || elem n stk)+           = (not inl || elem n stk)              || (n == sUN "prim__syntactic_eq")        | otherwise = False -    getCases cd | simpl = cases_totcheck cd+    getCases cd | simpl = cases_compiletime cd                 | runtime = cases_runtime cd                 | otherwise = cases_compiletime cd      ev ntimes stk top env (P _ n ty)         | Just (Let t v) <- lookup n genv = ev ntimes stk top env v     ev ntimes_in stk top env (P Ref n ty)-      | not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)-      | otherwise          = do let limit = if simpl then 100 else 10000-              (u, ntimes) <- usable spec limit n ntimes_in-              let red = u && (tcReducible n ctxt || spec || atRepl || runtime+              (u, ntimes) <- usable spec unfold limit n ntimes_in+              let red = u && (tcReducible n ctxt || spec || atRepl +                                || runtime || unfold                                 || sUN "assert_total" `elem` stk)               if red then-               do let val = lookupDefAcc n (spec || atRepl || runtime) ctxt+               do let val = lookupDefAccExact n (spec || unfold || atRepl || runtime) ctxt                   case val of-                    [(Function _ tm, Public)] ->+                    Just (Function _ tm, Public) ->                            ev ntimes (n:stk) True env tm-                    [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty-                                              return $ VP nt n vty-                    [(CaseOp ci _ _ _ _ cd, acc)]-                         | (acc == Public || acc == Hidden || sUN "assert_total" `elem` stk) &&-                             null (fst (cases_totcheck cd)) -> -- unoptimised version+                    Just (TyDecl nt ty, _) -> do vty <- ev ntimes stk True env ty+                                                 return $ VP nt n vty+                    Just (CaseOp ci _ _ _ _ cd, acc)+                         | (acc == Public || acc == Hidden) &&+--                                || sUN "assert_total" `elem` stk) &&+                             null (fst (cases_compiletime cd)) -> -- unoptimised version                        let (ns, tree) = getCases cd in                          if blockSimplify ci n stk                             then liftM (VP Ref n) (ev ntimes stk top env ty)@@ -281,12 +299,12 @@                     _ -> liftM (VP Ref n) (ev ntimes stk top env ty)                else liftM (VP Ref n) (ev ntimes stk top env ty)     ev ntimes stk top env (P nt n ty)-         = liftM (VP nt n) (ev ntimes stk top env ty)+        = liftM (VP nt n) (ev ntimes stk top env ty)     ev ntimes stk top env (V i)-                     | i < length env && i >= 0 = return $ snd (env !! i)-                     | otherwise      = return $ VV i+        | i < length env && i >= 0 = return $ snd (env !! i)+        | otherwise      = return $ VV i     ev ntimes stk top env (Bind n (Let t v) sc)-        | not runtime || occurrences n sc < 2+        | (not (runtime || simpl_inline || unfold)) || occurrences n sc < 2            = do v' <- ev ntimes stk top env v --(finalise v)                 sc' <- ev ntimes stk top ((n, v') : env) sc                 wknV (-1) sc'@@ -315,7 +333,7 @@     -- block reduction immediately under codata (and not forced)     ev ntimes stk top env               (App _ (App _ (App _ d@(P _ (UN dly) _) l@(P _ (UN lco) _)) t) arg)-       | dly == txt "Delay" && lco == txt "Infinite" && not simpl+       | dly == txt "Delay" && lco == txt "Infinite" && not (unfold || simpl)             = do let (f, _) = unApply arg                  let ntimes' = case f of                                     P _ fn _ -> (fn, 0) : ntimes@@ -329,8 +347,8 @@                  evApply ntimes' stk top env [l',t',arg'] d'     -- Treat "assert_total" specially, as long as it's defined!     ev ntimes stk top env (App _ (App _ (P _ n@(UN at) _) _) arg)-       | [(CaseOp _ _ _ _ _ _, _)] <- lookupDefAcc n (spec || atRepl || runtime) ctxt,-         at == txt "assert_total" && not simpl+       | Just (CaseOp _ _ _ _ _ _, _) <- lookupDefAccExact n (spec || atRepl || runtime) ctxt,+         at == txt "assert_total" && not (simpl || unfold)             = ev ntimes (n : stk) top env arg     ev ntimes stk top env (App _ f a)            = do f' <- ev ntimes stk False env f@@ -348,6 +366,7 @@     ev ntimes stk top env (Constant c) = return $ VConstant c     ev ntimes stk top env Erased    = return VErased     ev ntimes stk top env Impossible  = return VImpossible+    ev ntimes stk top env (Inferred tm) = ev ntimes stk top env tm     ev ntimes stk top env (TType i)   = return $ VType i     ev ntimes stk top env (UType u)   = return $ VUType u @@ -357,9 +376,9 @@           = apply ntimes stk top env f args      reapply ntimes stk top env f@(VP Ref n ty) args-       = let val = lookupDefAcc n (spec || atRepl || runtime) ctxt in+       = let val = lookupDefAccExact n (spec || atRepl || runtime) ctxt in          case val of-              [(CaseOp ci _ _ _ _ cd, acc)] ->+              Just (CaseOp ci _ _ _ _ cd, acc) ->                  let (ns, tree) = getCases cd in                      do c <- evCase ntimes n (n:stk) top env ns args tree                         case c of@@ -377,18 +396,15 @@               app <- apply ntimes stk top env a' as               wknV 1 app     apply ntimes_in stk top env f@(VP Ref n ty) args-      | not top && hnf = case args of-                            [] -> return f-                            _ -> return $ unload env f args-      | otherwise          = do let limit = if simpl then 100 else 10000-              (u, ntimes) <- usable spec limit n ntimes_in-              let red = u && (tcReducible n ctxt || spec || atRepl || runtime+              (u, ntimes) <- usable spec unfold limit n ntimes_in+              let red = u && (tcReducible n ctxt || spec || atRepl +                                || unfold || runtime                                 || sUN "assert_total" `elem` stk)               if red then-                 do let val = lookupDefAcc n (spec || atRepl || runtime) ctxt+                 do let val = lookupDefAccExact n (spec || unfold || atRepl || runtime) ctxt                     case val of-                      [(CaseOp ci _ _ _ _ cd, acc)]+                      Just (CaseOp ci _ _ _ _ cd, acc)                            | acc == Public || acc == Hidden ->                            -- unoptimised version                        let (ns, tree) = getCases cd in@@ -399,7 +415,7 @@                                    case c of                                       (Nothing, _) -> return $ unload env (VP Ref n ty) args                                       (Just v, rest) -> evApply ntimes stk top env rest v-                      [(Operator _ i op, _)]  ->+                      Just (Operator _ i op, _)  ->                         if (i <= length args)                            then case op (take i args) of                               Nothing -> return $ unload env (VP Ref n ty) args@@ -687,7 +703,7 @@                                        caseeq ((x,y):ps) xdef ydef                         _ -> return False -    sameCase :: [(Name, Name)] -> Name -> Name -> [Term] -> [Term] -> +    sameCase :: [(Name, Name)] -> Name -> Name -> [Term] -> [Term] ->                 StateT UCs TC Bool     sameCase ps x y xargs yargs           = case (lookupDef x ctxt, lookupDef y ctxt) of@@ -697,7 +713,7 @@                   [CaseOp _ _ _ _ _ yd])                        -> let (xin, xdef) = cases_compiletime xd                               (yin, ydef) = cases_compiletime yd in-                            do liftM2 (&&) +                            do liftM2 (&&)                                   (do ok <- zipWithM (ceq ps)                                               (drop (length xin) xargs)                                               (drop (length yin) yargs)@@ -734,9 +750,7 @@ --                   [Name] SC -- Run time cae definitions  data CaseDefs = CaseDefs {-                  cases_totcheck :: !([Name], SC),                   cases_compiletime :: !([Name], SC),-                  cases_inlined :: !([Name], SC),                   cases_runtime :: !([Name], SC)                 }   deriving Generic@@ -764,11 +778,8 @@     show (Operator ty _ _) = "Operator: " ++ show ty     show (CaseOp (CaseInfo inlc inla inlr) ty atys ps_in ps cd)       = let (ns, sc) = cases_compiletime cd-            (ns_t, sc_t) = cases_totcheck cd             (ns', sc') = cases_runtime cd in           "Case: " ++ show ty ++ " " ++ show ps ++ "\n" ++-                                        "TOTALITY CHECK TIME:\n\n" ++-                                        show ns_t ++ " " ++ show sc_t ++ "\n\n" ++                                         "COMPILE TIME:\n\n" ++                                         show ns ++ " " ++ show sc ++ "\n\n" ++                                         "RUN TIME:\n\n" ++@@ -928,42 +939,37 @@               [(Type, Bool)] -> -- argument types, whether canonical               [Int] ->  -- inaccessible arguments               [Either Term (Term, Term)] ->-              [([Name], Term, Term)] -> -- totality               [([Name], Term, Term)] -> -- compile time-              [([Name], Term, Term)] -> -- inlined               [([Name], Term, Term)] -> -- run time               Type -> Context -> TC Context addCasedef n ei ci@(CaseInfo inline alwaysInline tcdict)            tcase covering reflect asserted argtys inacc-           ps_in ps_tot ps_inl ps_ct ps_rt ty uctxt+           ps_in ps_ct ps_rt ty uctxt     = do let ctxt = definitions uctxt              access = case lookupDefAcc n False uctxt of                            [(_, acc)] -> acc                            _ -> Public-         totalityTime <- simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_tot ei          compileTime <- simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_ct ei-         inlined <- simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_inl ei          runtime <- simpleCase tcase covering reflect RunTime emptyFC inacc argtys ps_rt ei-         ctxt' <- case (totalityTime, compileTime, inlined, runtime) of-                    (CaseDef args_tot sc_tot _,-                     CaseDef args_ct sc_ct _,-                     CaseDef args_inl sc_inl _,+         ctxt' <- case (compileTime, runtime) of+                    ( CaseDef args_ct sc_ct _,                      CaseDef args_rt sc_rt _) ->                        let inl = alwaysInline -- tcdict                            inlc = (inl || small n args_ct sc_ct) && (not asserted)                            inlr = inl || small n args_rt sc_rt-                           cdef = CaseDefs (args_tot, sc_tot)-                                           (args_ct, sc_ct)-                                           (args_inl, sc_inl)+                           cdef = CaseDefs (args_ct, sc_ct)                                            (args_rt, sc_rt)                            op = (CaseOp (ci { case_inlinable = inlc })-                                                ty argtys ps_in ps_tot cdef,+                                                ty argtys ps_in ps_ct cdef,                                  False, access, Unchecked, EmptyMI)                        in return $ addDef n op ctxt --                    other -> tfail (Msg $ "Error adding case def: " ++ show other)          return uctxt { definitions = ctxt' } --- simplify a definition for totality checking+-- simplify a definition by inlining+-- (Note: This used to be for totality checking, and now it's actually a+-- no-op, but I'm keeping it here because I'll be putting it back with some+-- more carefully controlled inlining at some stage. --- EB) simplifyCasedef :: Name -> ErasureInfo -> Context -> TC Context simplifyCasedef n ei uctxt    = do let ctxt = definitions uctxt@@ -975,7 +981,7 @@                              pdef = map debind ps_in'                          CaseDef args sc _ <- simpleCase False (STerm Erased) False CompileTime emptyFC [] atys pdef ei                          return $ addDef n (CaseOp ci-                                              ty atys ps_in' ps (cd { cases_totcheck = (args, sc) }),+                                              ty atys ps_in' ps (cd { cases_compiletime = (args, sc) }),                                               inj, acc, tot, metainf) ctxt                     _ -> return ctxt@@ -989,7 +995,7 @@                                 (vs, x', y')     debind (Left x)       = let (vs, x') = depat [] x in                                 (vs, x', Impossible)-    simpl (Right (x, y)) = Right (x, simplify uctxt [] y)+    simpl (Right (x, y)) = Right (x, y) -- inline uctxt [] y)     simpl t = t  addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) ->

@@ -6,48 +6,43 @@ Maintainer  : The Idris Community. -} -{-# LANGUAGE PatternGuards, ExistentialQuantification, CPP #-}+{-# LANGUAGE CPP, ExistentialQuantification, PatternGuards #-} {-# OPTIONS_GHC -fwarn-incomplete-patterns #-} module Idris.Core.Execute (execute) where  import Idris.AbsSyntax import Idris.AbsSyntaxTree-import IRTS.Lang(FDesc(..), FType(..))--import Idris.Primitives(Prim(..), primitives)--import Idris.Core.TT-import Idris.Core.Evaluate import Idris.Core.CaseTree-+import Idris.Core.Evaluate+import Idris.Core.TT import Idris.Error--import Debug.Trace+import Idris.Primitives (Prim(..), primitives)+import IRTS.Lang (FDesc(..), FType(..))  import Util.DynamicLinker import Util.System  import Control.Applicative hiding (Const) import Control.Exception+import Control.Monad hiding (forM) import Control.Monad.Trans-import Control.Monad.Trans.State.Strict import Control.Monad.Trans.Except (ExceptT, runExceptT, throwE)-import Control.Monad hiding (forM)-import Data.Maybe+import Control.Monad.Trans.State.Strict import Data.Bits-import Data.Traversable (forM)-import Data.Time.Clock.POSIX (getPOSIXTime) import qualified Data.Map as M+import Data.Maybe+import Data.Time.Clock.POSIX (getPOSIXTime)+import Data.Traversable (forM)+import Debug.Trace+import System.IO  #ifdef IDRIS_FFI-import Foreign.LibFFI import Foreign.C.String+import Foreign.LibFFI import Foreign.Marshal.Alloc (free) import Foreign.Ptr #endif -import System.IO- #ifndef IDRIS_FFI execute :: Term -> Idris Term execute tm = fail "libffi not supported, rebuild Idris with -f FFI"@@ -180,9 +175,9 @@          [Function _ tm] -> doExec env ctxt tm          [TyDecl _ _] -> return (EP Ref n EErased) -- abstract def          [Operator tp arity op] -> return (EP Ref n EErased) -- will be special-cased later-         [CaseOp _ _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun+         [CaseOp _ _ _ _ _ (CaseDefs ([], STerm tm) _)] -> -- nullary fun              doExec env ctxt tm-         [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] -> return (EP Ref n EErased)+         [CaseOp _ _ _ _ _ (CaseDefs (ns, sc) _)] -> return (EP Ref n EErased)          [] -> execFail . Msg $ "Could not find " ++ show n ++ " in definitions."          other | length other > 1 -> execFail . Msg $ "Multiple definitions found for " ++ show n                | otherwise        -> execFail . Msg . take 500 $ "got to " ++ show other ++ " lookup up " ++ show n@@ -217,6 +212,7 @@                               doExec env ctxt ((x:xs) !! i) doExec env ctxt Erased = return EErased doExec env ctxt Impossible = fail "Tried to execute an impossible case"+doExec env ctxt (Inferred t) = doExec env ctxt t doExec env ctxt (TType u) = return (EType u) doExec env ctxt (UType u) = return (EUType u) @@ -275,10 +271,10 @@                                            execApp env ctxt r (drop arity args)                       _ -> return (mkEApp f args)                else return (mkEApp f args)-         [CaseOp _ _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun+         [CaseOp _ _ _ _ _ (CaseDefs ([], STerm tm) _)] -> -- nullary fun              do rhs <- doExec env ctxt tm                 execApp env ctxt rhs args-         [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] ->+         [CaseOp _ _ _ _ _ (CaseDefs (ns, sc) _)] ->              do res <- execCase env ctxt ns sc args                 return $ fromMaybe (mkEApp f args) res          thing -> return $ mkEApp f args@@ -402,6 +398,12 @@                       "The argument to isNull should be a pointer or file handle or string, but it was " ++                       show ptr ++                       ". Are all cases covered?"++    | Just (FFun "idris_disableBuffering" _ _) <- foreignFromTT arity ty fn xs+       = do execIO $ hSetBuffering stdin NoBuffering+            execIO $ hSetBuffering stdout NoBuffering+            execApp env ctxt ioUnit (drop arity xs)+  -- Right now, there's no way to send command-line arguments to the executor, -- so just return 0.

@@ -10,7 +10,7 @@ evaluation/checking inside the proof system, etc. -} -{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, PatternGuards #-} module Idris.Core.ProofState(     ProofState(..), newProof, envAtFocus, goalAtFocus   , Tactic(..), Goal(..), processTactic, nowElaboratingPS@@ -18,20 +18,21 @@   , keepGiven, getProvenance   ) where -import Idris.Core.Typecheck import Idris.Core.Evaluate+import Idris.Core.ProofTerm import Idris.Core.TT+import Idris.Core.Typecheck import Idris.Core.Unify-import Idris.Core.ProofTerm+import Idris.Core.WHNF -import Control.Monad.State.Strict+import Util.Pretty hiding (fill)+ import Control.Applicative hiding (empty) import Control.Arrow ((***))+import Control.Monad.State.Strict import Data.List import Debug.Trace -import Util.Pretty hiding (fill)- data ProofState = PS { thname            :: Name,                        holes             :: [Name], -- ^ holes still to be solved                        usedns            :: [Name], -- ^ used names, don't use again@@ -81,7 +82,8 @@             | Compute             | ComputeLet Name             | Simplify-            | HNF_Compute+            | WHNF_Compute+            | WHNF_ComputeArgs             | EvalIn Raw             | CheckIn Raw             | Intro (Maybe Name)@@ -651,7 +653,7 @@                   Nothing -> x        let t' = case t of                     x@(Bind y (Pi _ s _) _) -> x-                    _ -> hnf ctxt env t+                    _ -> normalise ctxt env t        (tyv, tyt) <- lift $ check ctxt env ty --        ns <- lift $ unify ctxt env tyv t'        case t' of@@ -668,7 +670,7 @@ intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =     do let t' = case t of                     x@(Bind y (Pi _ s _) _) -> x-                    _ -> hnf ctxt env t+                    _ -> normalise ctxt env t        case t' of            Bind y (Pi _ s _) t ->                let n = case mn of@@ -825,7 +827,7 @@ patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =     do let t' = case t of                     x@(Bind y (PVTy s) t) -> x-                    _ -> hnf ctxt env t+                    _ -> normalise ctxt env t        case t' of            Bind y (PVTy s) t -> let t' = updsubst y (P Bound n s) t in                                     return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))@@ -837,13 +839,18 @@     do return $ Bind x (Hole (normalise ctxt env ty)) sc compute ctxt env t = return t -hnf_compute :: RunTactic-hnf_compute ctxt env (Bind x (Hole ty) sc) =-    do let ty' = hnf ctxt env ty in---          trace ("HNF " ++ show (ty, ty')) $+whnf_compute :: RunTactic+whnf_compute ctxt env (Bind x (Hole ty) sc) =+    do let ty' = whnf ctxt env ty in            return $ Bind x (Hole ty') sc-hnf_compute ctxt env t = return t+whnf_compute ctxt env t = return t +whnf_compute_args :: RunTactic+whnf_compute_args ctxt env (Bind x (Hole ty) sc) =+    do let ty' = whnfArgs ctxt env ty in+           return $ Bind x (Hole ty') sc+whnf_compute_args ctxt env t = return t+ -- reduce let bindings only simplify :: RunTactic simplify ctxt env (Bind x (Hole ty) sc) =@@ -1131,7 +1138,8 @@          mktac (StartUnify n)    = start_unify n          mktac Compute           = compute          mktac Simplify          = Idris.Core.ProofState.simplify-         mktac HNF_Compute       = hnf_compute+         mktac WHNF_Compute      = whnf_compute+         mktac WHNF_ComputeArgs  = whnf_compute_args          mktac (Intro n)         = intro n          mktac (IntroTy ty n)    = introTy ty n          mktac (Forall n i t)    = forall n i t

@@ -6,7 +6,7 @@ Maintainer  : The Idris Community. -} -{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, PatternGuards #-} module Idris.Core.ProofTerm(     ProofTerm, Goal(..), mkProofTerm, getProofTerm   , resetProofTerm@@ -16,9 +16,9 @@   , goal, atHole   ) where -import Idris.Core.Typecheck import Idris.Core.Evaluate import Idris.Core.TT+import Idris.Core.Typecheck  import Control.Monad.State.Strict import Data.List

@@ -22,8 +22,8 @@    * We have a simple collection of tactics which we use to elaborate source      programs with implicit syntax into fully explicit terms. -}-{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor,-             DeriveDataTypeable, DeriveGeneric, PatternGuards #-}+{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveGeneric,+             FunctionalDependencies, MultiParamTypeClasses, PatternGuards #-} {-# OPTIONS_GHC -fwarn-incomplete-patterns #-} module Idris.Core.TT(     AppStatus(..), ArithTy(..), Binder(..), Const(..), Ctxt(..)@@ -38,7 +38,7 @@   , bindingOf, bindTyArgs, caseName, constDocs, constIsType, deleteDefExact   , discard, emptyContext, emptyFC, explicitNames, fc_end, fc_fname   , fc_start, fcIn, fileFC, finalise, fmapMB, forget, forgetEnv-  , freeNames, getArgTys, getRetTy, implicitable, instantiate, internalNS+  , freeNames, getArgTys, getRetTy, substRetTy, implicitable, instantiate, internalNS   , intTyName, isInjective, isTypeConst, lookupCtxt   , lookupCtxtExact, lookupCtxtName, mapCtxt, mkApp, nativeTyWidth   , nextName, noOccurrence, nsroot, occurrences@@ -51,40 +51,39 @@   , uniqueNameFrom, uniqueNameSet, unList, updateDef, vToP, weakenTm   ) where +import Util.Pretty hiding (Str)+ -- Work around AMP without CPP-import Prelude (Eq(..), Show(..), Ord(..), Functor(..), Monad(..), String, Int,-                Integer, Ordering(..), Maybe(..), Num(..), Bool(..), Enum(..),-                Read(..), FilePath, Double, (&&), (||), ($), (.), div, error, flip,-                fst, snd, not, mod, read, otherwise)+import Prelude (Bool(..), Double, Enum(..), Eq(..), FilePath, Functor(..), Int,+                Integer, Maybe(..), Monad(..), Num(..), Ord(..), Ordering(..),+                Read(..), Show(..), String, div, error, flip, fst, mod, not,+                otherwise, read, snd, ($), (&&), (.), (||)) -import Control.Applicative (Applicative (..), Alternative)-import qualified Control.Applicative as A (Alternative (..))+import Control.Applicative (Alternative, Applicative(..))+import qualified Control.Applicative as A (Alternative(..)) import Control.DeepSeq (($!!)) import Control.Monad.State.Strict-import Control.Monad.Trans.Except (Except (..))-import Debug.Trace-import qualified Data.Map.Strict as Map+import Control.Monad.Trans.Except (Except(..))+import Data.Binary hiding (get, put)+import qualified Data.Binary as B import Data.Char import Data.Data (Data)-import Data.Monoid (mconcat)-import Numeric (showIntAtBase)-import qualified Data.Text as T+import Data.Foldable (Foldable) import Data.List hiding (group, insert)-import Data.Set(Set, member, fromList, insert)+import qualified Data.Map.Strict as Map import Data.Maybe (listToMaybe)-import Data.Foldable (Foldable)+import Data.Monoid (mconcat)+import Data.Set (Set, fromList, insert, member)+import qualified Data.Text as T import Data.Traversable (Traversable) import Data.Typeable (Typeable) import Data.Vector.Unboxed (Vector) import qualified Data.Vector.Unboxed as V-import qualified Data.Binary as B-import Data.Binary hiding (get, put)+import Debug.Trace import Foreign.Storable (sizeOf) import GHC.Generics (Generic)--import Numeric.IEEE (IEEE (identicalIEEE))--import Util.Pretty hiding (Str)+import Numeric (showIntAtBase)+import Numeric.IEEE (IEEE(identicalIEEE))  data Option = TTypeInTType             | CheckConv@@ -235,7 +234,7 @@                      | TermPart Term                      | RawPart Raw                      | SubReport [ErrorReportPart]-                       deriving (Show, Eq, Data, Generic, Typeable)+                       deriving (Show, Eq, Ord, Data, Generic, Typeable)   data Provenance = ExpectedType@@ -243,7 +242,7 @@                 | InferredVal                 | GivenVal                 | SourceTerm Term-  deriving (Show, Eq, Data, Generic, Typeable)+  deriving (Show, Eq, Ord, Data, Generic, Typeable) {-! deriving instance Binary Err !-}@@ -308,7 +307,7 @@           | RunningElabScript (Err' t) -- ^ The error occurred during a top-level elaboration script           | ElabScriptStaging Name           | FancyMsg [ErrorReportPart]-  deriving (Eq, Functor, Data, Generic, Typeable)+  deriving (Eq, Ord, Functor, Data, Generic, Typeable)  type Err = Err' Term @@ -821,7 +820,7 @@          | RType          | RUType Universe          | RConstant Const-  deriving (Show, Eq, Data, Generic, Typeable)+  deriving (Show, Eq, Ord, Data, Generic, Typeable)  instance Sized Raw where   size (Var name) = 1@@ -941,7 +940,7 @@   size _ = 1  instance Show UExp where-    show (UVar ns x) +    show (UVar ns x)        | x < 26 = ns ++ "." ++ [toEnum (x + fromEnum 'a')]        | otherwise = ns ++ "." ++ toEnum ((x `mod` 26) + fromEnum 'a') : show (x `div` 26)     show (UVal x) = show x@@ -1009,6 +1008,9 @@                              -- (-1) is a special case for 'subtract one from BI'           | Erased -- ^ an erased term           | Impossible -- ^ special case for totality checking+          | Inferred (TT n) -- ^ For building case trees when coverage checkimg only.+                            -- Marks a term as being inferred by the machine, rather than+                            -- given by the programmer           | TType UExp -- ^ the type of types at some level           | UType Universe -- ^ Uniqueness type universe (disjoint from TType)   deriving (Ord, Functor, Data, Generic, Typeable)@@ -1056,6 +1058,7 @@   size (TType u) = 1 + size u   size (Proj a _) = 1 + size a   size Impossible = 1+  size (Inferred t) = size t   size (UType u) = 1 + size u  instance Pretty a o => Pretty (TT a) o where@@ -1289,7 +1292,7 @@   st (Bind x b sc) = Bind x (fmap st b) (st sc)   st t = t -  eqAlpha as (P _ x _) (P _ y _) +  eqAlpha as (P _ x _) (P _ y _)        = x == y || (x, y) `elem` as || (y, x) `elem` as   eqAlpha as (V x) (V y) = x == y   eqAlpha as (Bind x xb xs) (Bind y yb ys)@@ -1301,7 +1304,7 @@        = eqAlpha as xt yt && eqAlpha as xv yv   eqAlphaB as (Guess xt xv) (Guess yt yv)        = eqAlpha as xt yt && eqAlpha as xv yv-  eqAlphaB as bx by = eqAlpha as (binderTy bx) (binderTy by) +  eqAlphaB as bx by = eqAlpha as (binderTy bx) (binderTy by)  -- | Return number of occurrences of V 0 or bound name i the term occurrences :: Eq n => n -> TT n -> Int@@ -1380,6 +1383,7 @@ termSmallerThan x (Constant c) = True termSmallerThan x Erased = True termSmallerThan x Impossible = True+termSmallerThan x (Inferred t) = termSmallerThan x t termSmallerThan x (TType u) = True termSmallerThan x (UType u) = True @@ -1422,6 +1426,7 @@ safeForgetEnv env Erased    = Just $ RConstant Forgot safeForgetEnv env (Proj tm i) = error "Don't know how to forget a projection" safeForgetEnv env Impossible = error "Don't know how to forget Impossible"+safeForgetEnv env (Inferred t) = safeForgetEnv env t  -- | Introduce a 'Bind' into the given term for each element of the -- given list of (name, binder) pairs.@@ -1450,6 +1455,14 @@ getRetTy (Bind n (Pi _ _ _) sc)   = getRetTy sc getRetTy sc = sc +-- | As getRetTy but substitutes names for de Bruijn indices+substRetTy :: TT n -> TT n+substRetTy (Bind n (PVar ty) sc) = substRetTy (substV (P Ref n ty) sc)+substRetTy (Bind n (PVTy ty) sc) = substRetTy (substV (P Ref n ty) sc)+substRetTy (Bind n (Pi _ ty _) sc) = substRetTy (substV (P Ref n ty) sc)+substRetTy sc = sc+   + uniqueNameFrom :: [Name] -> [Name] -> Name uniqueNameFrom []           hs = uniqueName (nextName (sUN "x")) hs uniqueNameFrom (s : supply) hs@@ -1576,6 +1589,7 @@     prettySe p env Erased debug = text "[_]"     prettySe p env (TType i) debug = text "Type" <+> (text . show $ i)     prettySe p env Impossible debug = text "Impossible"+    prettySe p env (Inferred tm) debug = text "<" <+> prettySe p env tm debug <+> text ">"     prettySe p env (UType u) debug = text (show u)      -- Render a `Binder` and its name@@ -1621,6 +1635,7 @@     se p env (Constant c) = show c     se p env Erased = "[__]"     se p env Impossible = "[impossible]"+    se p env (Inferred t) = "<" ++ se p env t ++ ">"     se p env (TType i) = "Type " ++ show i     se p env (UType u) = show u @@ -1729,6 +1744,7 @@       text "!" <> text (show i)     pp p bound Erased = text "<<<erased>>>"     pp p bound Impossible = text "<<<impossible>>>"+    pp p bound (Inferred t) = text "<" <+> pp p bound t <+> text ">"     pp p bound (TType ue) = annotate (AnnType "Type" "The type of types") $                             text "Type"     pp p bound (UType u) = text (show u)

@@ -6,17 +6,17 @@ Maintainer  : The Idris Community. -} -{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,+{-# LANGUAGE DeriveFunctor, FlexibleInstances, MultiParamTypeClasses,              PatternGuards #-}  module Idris.Core.Typecheck where +import Idris.Core.Evaluate+import Idris.Core.TT+ import Control.Monad.State-import Debug.Trace import qualified Data.Vector.Unboxed as V (length)--import Idris.Core.TT-import Idris.Core.Evaluate+import Debug.Trace  -- To check conversion, normalise each term wrt the current environment. -- Since we haven't converted everything to de Bruijn indices yet, we'll have to@@ -83,7 +83,7 @@ check :: Context -> Env -> Raw -> TC (Term, Type) check ctxt env tm      -- Holes allowed, so constraint namespace doesn't matter-     = evalStateT (check' True [] ctxt env tm) (0, []) +     = evalStateT (check' True [] ctxt env tm) (0, [])  check' :: Bool -> String -> Context -> Env -> Raw -> StateT UCs TC (Term, Type) check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) Nothing env top where@@ -116,7 +116,7 @@            let fty' = case uniqueBinders (map fst env) (finalise fty) of                         ty@(Bind x (Pi i s k) t) -> ty                         _ -> uniqueBinders (map fst env)-                                 $ case hnf ctxt env fty of+                                 $ case normalise ctxt env fty of                                      ty@(Bind x (Pi i s k) t) -> ty                                      _ -> normalise ctxt env fty            case fty' of@@ -138,7 +138,7 @@            let fty' = case uniqueBinders (map fst env) (finalise fty) of                         ty@(Bind x (Pi i s k) t) -> ty                         _ -> uniqueBinders (map fst env)-                                 $ case hnf ctxt env fty of+                                 $ case normalise ctxt env fty of                                      ty@(Bind x (Pi i s k) t) -> ty                                      _ -> normalise ctxt env fty            (av, aty) <- chk u Nothing env a@@ -343,7 +343,7 @@                      StateT [(Name, (UniqueUse, Universe))] TC ()     chkBinderName env n b        = do let rawty = forgetEnv (map fst env) (binderTy b)-            (_, kind) <- lift $ check ctxt env rawty +            (_, kind) <- lift $ check ctxt env rawty             case kind of                  UType UniqueType -> do ns <- get                                         if n `elem` borrowed

@@ -19,13 +19,13 @@   , unrecoverable   ) where -import Idris.Core.TT import Idris.Core.Evaluate+import Idris.Core.TT  import Control.Monad import Control.Monad.State.Strict-import Data.Maybe import Data.List+import Data.Maybe import Debug.Trace  -- terms which need to be injective, with the things we're trying to unify

@@ -8,18 +8,19 @@  {-# LANGUAGE PatternGuards #-} {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}-module Idris.Core.WHNF(whnf, WEnv) where+module Idris.Core.WHNF(whnf, whnfArgs, WEnv) where -import Idris.Core.TT import Idris.Core.CaseTree import Idris.Core.Evaluate hiding (quote) import qualified Idris.Core.Evaluate as Evaluate+import Idris.Core.TT  import Debug.Trace  -- | A stack entry consists of a term and the environment it is to be -- evaluated in (i.e. it's a thunk) type StackEntry = (Term, WEnv)+ data WEnv = WEnv Int -- number of free variables                  [(Term, WEnv)]   deriving Show@@ -34,10 +35,11 @@ -- environment it was encountered in, so that when we quote back to a term -- we get the substitutions right. -data WHNF = WDCon Int Int Bool Name (Type, WEnv) -- ^ data constructor+data WHNF = WDCon Int Int Bool Name (Term, WEnv) -- ^ data constructor           | WTCon Int Int Name (Type, WEnv) -- ^ type constructor-          | WPRef Name (Type, WEnv) -- ^irreducible global (e.g. a postulate)-          | WBind Name (Binder Term) (Term, WEnv)+          | WPRef Name (Term, WEnv) -- ^irreducible global (e.g. a postulate)+          | WV Int+          | WBind Name (Binder (Term, WEnv)) (Term, WEnv)           | WApp WHNF (Term, WEnv)           | WConstant Const           | WProj WHNF Int@@ -46,24 +48,56 @@           | WErased           | WImpossible --- | Reduce a *closed* term to weak head normal form.-whnf :: Context -> Term -> Term-whnf ctxt tm = quote (do_whnf ctxt (WEnv 0 []) tm)+-- NOTE: These aren't yet ready to be used in practice - there's still a+-- bug or two in the handling of de Bruijn indices. -do_whnf :: Context -> WEnv -> Term -> WHNF-do_whnf ctxt env tm = eval env [] tm+-- | Reduce a term to weak head normal form.+whnf :: Context -> Env -> Term -> Term+-- whnf ctxt env tm = let res = whnf' ctxt env tm in+--                        trace (show tm ++ "\n==>\n" ++ show res ++ "\n") res+whnf ctxt env tm = +   inlineSmall ctxt env $ -- reduce small things in body. This is primarily+                          -- to get rid of any noisy "assert_smaller/assert_total"+                          -- and evaluate any simple operators, which makes things+                          -- easier to read.+     whnf' ctxt env tm+whnf' ctxt env tm = +     quote (do_whnf ctxt (map finalEntry env) (finalise tm))++-- | Reduce a type so that all arguments are expanded+whnfArgs :: Context -> Env -> Term -> Term+whnfArgs ctxt env tm = inlineSmall ctxt env $ finalise (whnfArgs' ctxt env tm)+whnfArgs' ctxt env tm+    = case whnf' ctxt env tm of+           -- The assumption is that de Bruijn indices refer to local things+           -- (so not in the external environment) so we need to instantiate+           -- the name+           Bind n b@(Pi _ ty _) sc -> +                    Bind n b (whnfArgs' ctxt ((n,b):env) +                             (subst n (P Bound n ty) sc))+           res -> tm++finalEntry :: (Name, Binder (TT Name)) -> (Name, Binder (TT Name))+finalEntry (n, b) = (n, fmap finalise b)++do_whnf :: Context -> Env -> Term -> WHNF+do_whnf ctxt genv tm = eval (WEnv 0 []) [] tm   where     eval :: WEnv -> Stack -> Term -> WHNF     eval wenv@(WEnv d env) stk (V i)          | i < length env = let (tm, env') = env !! i in                                 eval env' stk tm-         | otherwise = error "Can't happen: WHNF scope error"+         | otherwise = WV i     eval wenv@(WEnv d env) stk (Bind n (Let t v) sc)          = eval (WEnv d ((v, wenv) : env)) stk sc-    eval (WEnv d env) [] (Bind n b sc) = WBind n b (sc, WEnv (d + 1) env)-    eval (WEnv d env) ((tm, tenv) : stk) (Bind n b sc)+    eval (WEnv d env) ((tm, tenv) : stk) (Bind n b@(Lam _) sc)          = eval (WEnv d ((tm, tenv) : env)) stk sc+    eval wenv@(WEnv d env) stk (Bind n b sc) -- stk must be empty if well typed+         =let n' = uniqueName n (map fst genv) in+              WBind n' (fmap (\t -> (t, wenv)) b) (sc, WEnv (d + 1) env) +    eval env stk (P nt n ty) +         | Just (Let t v) <- lookup n genv = eval env stk v     eval env stk (P nt n ty) = apply env nt n ty stk     eval env stk (App _ f a) = eval env ((a, env) : stk) f     eval env stk (Constant c) = unload (WConstant c) stk@@ -73,30 +107,34 @@      eval env stk Erased = unload WErased stk     eval env stk Impossible = unload WImpossible stk+    eval env stk (Inferred tm) = eval env stk tm     eval env stk (TType u) = unload (WType u) stk     eval env stk (UType u) = unload (WUType u) stk      apply :: WEnv -> NameType -> Name -> Type -> Stack -> WHNF-    apply env nt n ty stk+    apply env nt n ty stk            = let wp = case nt of                           DCon t a u -> WDCon t a u n (ty, env)                           TCon t a -> WTCon t a n (ty, env)                           Ref -> WPRef n (ty, env)                           _ -> WPRef n (ty, env)                         in-            case lookupDefExact n ctxt of-                 Just (CaseOp ci _ _ _ _ cd) ->-                      let (ns, tree) = cases_compiletime cd in-                          case evalCase env ns tree stk of-                               Just w -> w-                               Nothing -> unload wp stk-                 Just (Operator _ i op) ->+            if not (tcReducible n ctxt)+               then unload wp stk+               else case lookupDefAccExact n False ctxt of+                         Just (CaseOp ci _ _ _ _ cd, acc) +                             | acc == Public || acc == Hidden ->+                          let (ns, tree) = cases_compiletime cd in+                              case evalCase env ns tree stk of+                                   Just w -> w+                                   Nothing -> unload wp stk+                         Just (Operator _ i op, acc) ->                           if i <= length stk                              then case runOp env op (take i stk) (drop i stk) of                                   Just v -> v                                   Nothing -> unload wp stk                              else unload wp stk-                 _ -> unload wp stk+                         _ -> unload wp stk      unload :: WHNF -> Stack -> WHNF     unload f [] = f@@ -112,6 +150,8 @@                   -- aren't run on constants are themselves pretty ugly                   -- (it's prim__believe_me and prim__syntacticEq, for                   -- example) so let's not worry too much...+                  -- We will need to deal with believe_me before dropping this+                  -- into the type checker, though.                   Just val -> Just $ eval env rest (quoteTerm val)                   _ -> Nothing @@ -189,7 +229,9 @@ quote (WDCon t a u n (ty, env)) = P (DCon t a u) n (quoteEnv env ty) quote (WTCon t a n (ty, env)) = P (TCon t a) n (quoteEnv env ty) quote (WPRef n (ty, env)) = P Ref n (quoteEnv env ty)-quote (WBind n ty (sc, env)) = Bind n ty (quoteEnv env sc)+quote (WV i) = V i+quote (WBind n b (sc, env)) = Bind n (fmap (\ (t, env) -> quoteEnv env t) b) +                                     (quoteEnv env sc) quote (WApp f (a, env)) = App Complete (quote f) (quoteEnv env a) quote (WConstant c) = Constant c quote (WProj t i) = Proj (quote t) i@@ -201,10 +243,13 @@ quoteEnv :: WEnv -> Term -> Term quoteEnv (WEnv d ws) tm = qe' d ws tm   where+    -- d is number of free variables in the external environment+    -- (all bound in the scope of 'ws')     qe' d ts (V i)-        | i < d = V i-        | otherwise = let (tm, env) = ts !! (i - d) in-                          quoteEnv env tm+        | (i - d) < length ts && (i - d) >= 0+              = let (tm, env) = ts !! (i - d) in+                    quoteEnv env tm+        | otherwise = V i     qe' d ts (Bind n b sc)         = Bind n (fmap (qe' d ts) b) (qe' (d + 1) ts sc)     qe' d ts (App c f a)

@@ -1,921 +1,375 @@ {-| Module      : Idris.Coverage-Description : The coverage and totality checkers for Idris are in this module.-Copyright   :-License     : BSD3-Maintainer  : The Idris Community.--}-{-# LANGUAGE PatternGuards #-}-module Idris.Coverage where--import Idris.Core.TT-import Idris.Core.Evaluate-import Idris.Core.CaseTree--import Idris.AbsSyntax-import Idris.Delaborate-import Idris.Error-import Idris.Output (iWarn, iputStrLn)--import Data.Char-import Data.List-import Data.Either-import Data.Maybe-import Debug.Trace--import Control.Monad.State.Strict---- | Generate a pattern from an 'impossible' LHS.------ We need this to eliminate the pattern clauses which have been--- provided explicitly from new clause generation.-mkPatTm :: PTerm -> Idris Term-mkPatTm t = do i <- getIState-               let timp = addImpl' True [] [] [] i t-               evalStateT (toTT (mapPT deNS timp)) 0-  where-    toTT (PRef _ _ n) = do i <- lift getIState-                           case lookupNameDef n (tt_ctxt i) of-                                [(n', TyDecl nt _)] -> return $ P nt n' Erased-                                _ -> return $ P Ref n Erased-    toTT (PApp _ t args) = do t' <- toTT t-                              args' <- mapM (toTT . getTm) args-                              return $ mkApp t' args'-    toTT (PDPair _ _ _ l _ r) = do l' <- toTT l-                                   r' <- toTT r-                                   return $ mkApp (P Ref sigmaCon Erased) [Erased, Erased, l', r']-    toTT (PPair _ _ _ l r) = do l' <- toTT l-                                r' <- toTT r-                                return $ mkApp (P Ref pairCon Erased) [Erased, Erased, l', r']-    -- For alternatives, pick the first and drop the namespaces. It doesn't-    -- really matter which is taken since matching will ignore the namespace.-    toTT (PAlternative _ _ (a : as)) = toTT a-    toTT _ = do v <- get-                put (v + 1)-                return (P Bound (sMN v "imp") Erased)--    deNS (PRef f hl (NS n _)) = PRef f hl n-    deNS t = t---- | Given a list of LHSs, generate a extra clauses which cover the remaining--- cases. The ones which haven't been provided are marked 'absurd' so--- that the checker will make sure they can't happen.------ This will only work after the given clauses have been typechecked and the--- names are fully explicit!-genClauses :: FC -> Name -> [Term] -> [PTerm] -> Idris [PTerm]-genClauses fc n xs given-   = do i <- getIState-        let lhs_tms = map (\x -> flattenArgs $ delab' i x True True) xs-        -- if a placeholder was given, don't bother generating cases for it-        let lhs_tms' = zipWith mergePlaceholders lhs_tms-                          (map (stripUnmatchable i) (map flattenArgs given))-        let lhss = map pUnApply lhs_tms'-        nty <- case lookupTyExact n (tt_ctxt i) of-                    Just t -> return (normalise (tt_ctxt i) [] t)-                    _ -> fail "Can't happen - genClauses, lookupTyExact"--        let argss = transpose lhss-        let all_args = map (genAll i) (zip (genPH i nty) argss)-        logCoverage 5 $ "COVERAGE of " ++ show n-        logCoverage 5 $ "using type " ++ show nty-        logCoverage 5 $ "non-concrete args " ++ show (genPH i nty)--        logCoverage 5 $ show (lhs_tms, lhss)-        logCoverage 5 $ "Args are: " ++ show argss-        logCoverage 5 $ show (map length argss) ++ "\nAll args:\n" ++ show (map length all_args)-        logCoverage 10 $ "All args are: " ++ show all_args-        logCoverage 3 $ "Original: \n" ++-             showSep "\n" (map (\t -> showTmImpls (delab' i t True True)) xs)-        -- add an infinite supply of explicit arguments to update the possible-        -- cases for (the return type may be variadic, or function type, so-        -- there may be more case splitting that the idris_implicits record-        -- suggests)-        let parg = case lookupCtxt n (idris_implicits i) of-                        (p : _) ->-                          p ++ repeat (PExp 0 [] (sMN 0 "gcarg") Placeholder)-                        _       -> repeat (pexp Placeholder)-        let tryclauses = mkClauses parg all_args-        logCoverage 3 $ show (length tryclauses) ++ " initially to check"-        logCoverage 2 $ showSep "\n" (map (showTm i) tryclauses)-        let new = filter (noMatch i) (nub tryclauses)-        logCoverage 2 $ show (length new) ++ " clauses to check for impossibility"-        logCoverage 4 $ "New clauses: \n" ++ showSep "\n" (map (showTm i) new)---           ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)-        return new---         return (map (\t -> PClause n t [] PImpossible []) new)-  where getLHS i term-            | (f, args) <- unApply term = map (\t -> delab' i t True True) args-            | otherwise = []--        -- if an argument has a non-concrete type (i.e. it's a function-        -- that calculates something from a previous argument) we'll also-        -- need to generate a placeholder pattern for it since it could be-        -- anything based on earlier values-        genPH :: IState -> Type -> [Bool]-        genPH ist (Bind n (Pi _ ty _) sc) = notConcrete ist ty : genPH ist sc-        genPH ist ty = []--        notConcrete ist t | (P _ n _, args) <- unApply t,-                           not (isConName n (tt_ctxt ist)) = True-        notConcrete _ _ = False--        pUnApply (PApp _ f args) = map getTm args-        pUnApply _ = []--        flattenArgs (PApp fc (PApp _ f as) as')-             = flattenArgs (PApp fc f (as ++ as'))-        flattenArgs t = t--        -- Return whether the given clause matches none of the input clauses-        -- (xs)-        noMatch i tm = all (\x -> case matchClause i (stripUnmatchable i (delab' i x True True)) tm of-                                       Right ms -> False-                                       Left miss -> True) xs---        mergePlaceholders :: PTerm -> PTerm -> PTerm-        mergePlaceholders x Placeholder = Placeholder-        mergePlaceholders (PApp fc f args) (PApp fc' f' args')-            = PApp fc' f' (zipWith mergePArg args args')-           where mergePArg x y = let xtm = mergePlaceholders (getTm x) (getTm y) in-                                     x { getTm = xtm}-        mergePlaceholders x _ = x--        mkClauses :: [PArg] -> [[PTerm]] -> [PTerm]-        mkClauses parg args-            | all (== [Placeholder]) args = []-        mkClauses parg args-            = do args' <- mkArg args-                 let tm = PApp fc (PRef fc [] n) (zipWith upd args' parg)-                 return tm-          where-            mkArg :: [[PTerm]] -> [[PTerm]]-            mkArg [] = return []-            mkArg (a : as) = do a' <- a-                                as' <- mkArg as-                                return (a':as')---- | Does this error result rule out a case as valid when coverage checking?-validCoverageCase :: Context -> Err -> Bool-validCoverageCase ctxt (CantUnify _ (topx, _) (topy, _) e _ _)-    = let topx' = normalise ctxt [] topx-          topy' = normalise ctxt [] topy in-          not (sameFam topx' topy' || not (validCoverageCase ctxt e))-  where sameFam topx topy-            = case (unApply topx, unApply topy) of-                   ((P _ x _, _), (P _ y _, _)) -> x == y-                   _ -> False-validCoverageCase ctxt (InfiniteUnify _ _ _) = False-validCoverageCase ctxt (CantConvert _ _ _) = False-validCoverageCase ctxt (At _ e) = validCoverageCase ctxt e-validCoverageCase ctxt (Elaborating _ _ _ e) = validCoverageCase ctxt e-validCoverageCase ctxt (ElaboratingArg _ _ _ e) = validCoverageCase ctxt e-validCoverageCase ctxt _ = True---- | Check whether an error is recoverable in the sense needed for--- coverage checking.-recoverableCoverage :: Context -> Err -> Bool-recoverableCoverage ctxt (CantUnify r (topx, _) (topy, _) e _ _)-    = let topx' = normalise ctxt [] topx-          topy' = normalise ctxt [] topy in-          r || checkRec topx' topy'-  where -- different notion of recoverable than in unification, since we-        -- have no metavars -- just looking to see if a constructor is failing-        -- to unify with a function that may be reduced later-        checkRec (App _ f a) p@(P _ _ _) = checkRec f p-        checkRec p@(P _ _ _) (App _ f a) = checkRec p f-        checkRec fa@(App _ _ _) fa'@(App _ _ _)-            | (f, as) <- unApply fa,-              (f', as') <- unApply fa'-                 = if (length as /= length as')-                      then checkRec f f'-                      else checkRec f f' && and (zipWith checkRec as as')-        checkRec (P xt x _) (P yt y _) = x == y || ntRec xt yt-        checkRec _ _ = False--        ntRec x y | Ref <- x = True-                  | Ref <- y = True-                  | (Bound, Bound) <- (x, y) = True-                  | otherwise = False -- name is different, unrecoverable-recoverableCoverage ctxt (At _ e) = recoverableCoverage ctxt e-recoverableCoverage ctxt (Elaborating _ _ _ e) = recoverableCoverage ctxt e-recoverableCoverage ctxt (ElaboratingArg _ _ _ e) = recoverableCoverage ctxt e-recoverableCoverage _ _ = False--genAll :: IState -> (Bool, [PTerm]) -> [PTerm]-genAll i (addPH, args)-   = case filter (/=Placeholder) $ fnub $ mergePHs $ fnub (concatMap otherPats (fnub args)) of-          [] -> [Placeholder]-          xs -> ph xs-  where-    ph ts = if addPH then Placeholder : ts else ts--    -- Merge patterns with placeholders in other patterns, to ensure we've-    -- covered all possible generated cases-    -- e.g. if we have (True, _) (False, _) (_, True) (_, False) -    -- we should merge these to get (True, True), (False, False)-    -- (False, True) and (True, False)-    mergePHs :: [PTerm] -> [PTerm]-    mergePHs xs = mergePHs' xs xs--    mergePHs' [] all = []-    mergePHs' (x : xs) all = mergePH x all ++ mergePHs' xs all--    mergePH :: PTerm -> [PTerm] -> [PTerm]-    mergePH tm [] = []-    mergePH tm (x : xs) -          | Just merged <- mergePTerm tm x = merged : mergePH tm xs-          | otherwise = mergePH tm xs--    mergePTerm :: PTerm -> PTerm -> Maybe PTerm-    mergePTerm x Placeholder = Just x-    mergePTerm Placeholder x = Just x-    mergePTerm tm@(PRef fc1 hl1 n1) (PRef fc2 hl2 n2)-          | n1 == n2 = Just tm-    mergePTerm (PPair fc1 hl1 p1 x1 y1) (PPair fc2 hl2 p2 x2 y2)-          = do x <- mergePTerm x1 x2-               y <- mergePTerm y1 y2-               Just (PPair fc1 hl1 p1 x y)-    mergePTerm (PDPair fc1 hl1 p1 x1 t1 y1) (PDPair fc2 hl2 p2 x2 t2 y2)-          = do x <- mergePTerm x1 x2-               y <- mergePTerm y1 y2-               t <- mergePTerm t1 t2-               Just (PDPair fc1 hl1 p1 x t y)-    mergePTerm (PApp fc1 f1 args1) (PApp fc2 f2 args2)-          = do fm <- mergePTerm f1 f2-               margs <- mergeArgs args1 args2-               Just (PApp fc1 fm margs)-      where-        mergeArgs [] [] = Just []-        mergeArgs (a : as) (b : bs)-                  = do ma_in <- mergePTerm (getTm a) (getTm b)-                       let ma = a { getTm = ma_in }-                       mas <- mergeArgs as bs-                       Just (ma : mas)-        mergeArgs _ _ = Nothing-    mergePTerm x y | x == y = Just x-                   | otherwise = Nothing--    -- for every constant in a term (at any level) take next one to make sure-    -- that constants which are not explicitly handled are covered-    nextConst (PConstant fc c) = PConstant NoFC (nc' c)-    nextConst o = o--    nc' (I c) = I (c + 1)-    nc' (BI c) = BI (c + 1)-    nc' (Fl c) = Fl (c + 1)-    nc' (B8 c) = B8 (c + 1)-    nc' (B16 c) = B16 (c + 1)-    nc' (B32 c) = B32 (c + 1)-    nc' (B64 c) = B64 (c + 1)-    nc' (Ch c) = Ch (chr $ ord c + 1)-    nc' (Str c) = Str (c ++ "'")-    nc' o = o--    otherPats :: PTerm -> [PTerm]-    otherPats o@(PRef fc hl n) = ph $ ops fc n [] o-    otherPats o@(PApp _ (PRef fc hl n) xs) = ph $ ops fc n xs o-    otherPats o@(PPair fc hls _ l r)-        = ph $ ops fc pairCon-                ([pimp (sUN "A") Placeholder True,-                  pimp (sUN "B") Placeholder True] ++-                 [pexp l, pexp r]) o-    otherPats o@(PDPair fc hls p t _ v)-        = ph $ ops fc sigmaCon-                ([pimp (sUN "a") Placeholder True,-                  pimp (sUN "P") Placeholder True] ++-                 [pexp t,pexp v]) o-    otherPats o@(PConstant _ c) = ph [o, nextConst o]-    otherPats arg = return Placeholder--    ops fc n xs o-        | (TyDecl c@(DCon _ arity _) ty : _) <- lookupDef n (tt_ctxt i)-            = do xs' <- mapM otherPats (map getExpTm xs)-                 let p = resugar (PApp fc (PRef fc [] n) (zipWith upd xs' xs))-                 let tyn = getTy n (tt_ctxt i)-                 case lookupCtxt tyn (idris_datatypes i) of-                         (TI ns _ _ _ _ : _) -> p : map (mkPat fc) (ns \\ [n])-                         _ -> [p]-    ops fc n arg o = return Placeholder--    getExpTm (PImp _ True _ _ _) = Placeholder -- machine inferred, no point!-    getExpTm t = getTm t--    -- put it back to its original form-    resugar (PApp _ (PRef fc hl n) [_,_,t,v])-      | n == sigmaCon-        = PDPair fc [] TypeOrTerm (getTm t) Placeholder (getTm v)-    resugar (PApp _ (PRef fc hl n) [_,_,l,r])-      | n == pairCon-        = PPair fc [] IsTerm (getTm l) (getTm r)-    resugar t = t--    dropForce force (x : xs) i | i `elem` force-        = upd Placeholder x : dropForce force xs (i + 1)-    dropForce force (x : xs) i = x : dropForce force xs (i + 1)-    dropForce _ [] _ = []---    getTy n ctxt = case lookupTy n ctxt of-                          (t : _) -> case unApply (getRetTy t) of-                                        (P _ tyn _, _) -> tyn-                                        x -> error $ "Can't happen getTy 1 " ++ show (n, x)-                          _ -> error "Can't happen getTy 2"--    mkPat fc x = case lookupCtxt x (idris_implicits i) of-                      (pargs : _)-                         -> PApp fc (PRef fc [] x) (map (upd Placeholder) pargs)-                      _ -> error "Can't happen - genAll"--    fnub :: [PTerm] -> [PTerm]-    fnub xs = fnub' [] xs--    fnub' :: [PTerm] -> [PTerm] -> [PTerm]-    fnub' acc (x : xs) | x `qelem` acc = fnub' acc (filter (not.(quickEq x)) xs)-                       | otherwise = fnub' (x : acc) xs-    fnub' acc [] = acc--    -- quick check for constructor equality-    quickEq :: PTerm -> PTerm -> Bool-    quickEq (PConstant _ n) (PConstant _ n') = n == n'-    quickEq (PRef _ _ n) (PRef _ _ n') = n == n'-    quickEq (PPair _ _ _ l r) (PPair _ _ _ l' r') = quickEq l l' && quickEq r r'-    quickEq (PApp _ t as) (PApp _ t' as')-        | length as == length as'-           = quickEq t t' && and (zipWith quickEq (map getTm as) (map getTm as'))-    quickEq Placeholder Placeholder = True-    quickEq x y = False--    qelem :: PTerm -> [PTerm] -> Bool-    qelem x [] = False-    qelem x (y : ys) | x `quickEq` y = True-                     | otherwise = qelem x ys---upd :: t -> PArg' t -> PArg' t-upd p' p = p { getTm = p' }---- | Check whether function and all descendants cover all cases--- (partial is okay, as long as it's due to recursion)-checkAllCovering :: FC -> [Name] -> Name -> Name -> Idris ()-checkAllCovering fc done top n | not (n `elem` done)-   = do i <- get-        case lookupTotal n (tt_ctxt i) of-             [tot@(Partial NotCovering)] ->-                    do let msg = show top ++ " is " ++ show tot ++ " due to " ++ show n-                       putIState i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i }-                       addIBC (IBCTotCheckErr fc msg)-             [Partial _] ->-                case lookupCtxt n (idris_callgraph i) of-                     [cg] -> mapM_ (checkAllCovering fc (n : done) top)-                                   (calls cg)-                     _ -> return ()-             x -> return () -- stop if total-checkAllCovering _ _ _ _ = return ()---- | Check if, in a given group of type declarations mut_ns, the--- constructor cn : ty is strictly positive, and update the context--- accordingly-checkPositive :: [Name]       -- ^ the group of type declarations-              -> (Name, Type) -- ^ the constructor-              -> Idris Totality-checkPositive mut_ns (cn, ty')-    = do i <- getIState-         let ty = delazy' True (normalise (tt_ctxt i) [] ty')-         let p = cp i ty-         let tot = if p then Total (args ty) else Partial NotPositive-         let ctxt' = setTotal cn tot (tt_ctxt i)-         putIState (i { tt_ctxt = ctxt' })-         logCoverage 5 $ "Constructor " ++ show cn ++ " is " ++ show tot ++ " with " ++ show mut_ns-         addIBC (IBCTotal cn tot)-         return tot-  where-    args t = [0..length (getArgTys t)-1]--    cp i (Bind n (Pi _ aty _) sc)-         = posArg i aty && cp i sc-    cp i t | (P _ n' _ , args) <- unApply t,-             n' `elem` mut_ns = all noRec args-    cp i _ = True--    posArg ist (Bind _ (Pi _ nty _) sc) = noRec nty && posArg ist sc-    posArg ist t = posParams ist t--    noRec arg = all (\x -> x `notElem` mut_ns) (allTTNames arg)--    -- If the type appears recursively in a parameter argument, that's-    -- fine, otherwise if it appears in an argument it's not fine.-    posParams ist t | (P _ n _, args) <- unApply t-       = case lookupCtxtExact n (idris_datatypes ist) of-              Just ti -> checkParamsOK (param_pos ti) 0 args-              Nothing -> and (map (posParams ist) args)-    posParams ist t = noRec t--    checkParamsOK ppos i [] = True-    checkParamsOK ppos i (p : ps)-          | i `elem` ppos = checkParamsOK ppos (i + 1) ps-          | otherwise = noRec p && checkParamsOK ppos (i + 1) ps---- | Calculate the totality of a function from its patterns.  Either--- follow the size change graph (if inductive) or check for--- productivity (if coinductive)-calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality-calcTotality fc n pats-    = do i <- getIState-         let opts = case lookupCtxt n (idris_flags i) of-                            [fs] -> fs-                            _ -> []-         case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of-            (failure : _) -> return failure-            _ -> checkSizeChange n-  where-    checkLHS i (P _ fn _)-        = case lookupTotalExact fn (tt_ctxt i) of-               Just (Partial _) -> return (Partial (Other [fn]))-               _ -> Nothing-    checkLHS i (App _ f a) = mplus (checkLHS i f) (checkLHS i a)-    checkLHS _ _ = Nothing--checkTotality :: [Name] -> FC -> Name -> Idris Totality-checkTotality path fc n-    | n `elem` path = return (Partial (Mutual (n : path)))-    | otherwise = do-        t <- getTotality n-        i <- getIState-        ctxt' <- do ctxt <- getContext-                    tclift $ simplifyCasedef n (getErasureInfo i) ctxt-        setContext ctxt'-        ctxt <- getContext-        i <- getIState-        let opts = case lookupCtxt n (idris_flags i) of-                            [fs] -> fs-                            _ -> []-        t' <- case t of-                Unchecked ->-                    case lookupDef n ctxt of-                        [CaseOp _ _ _ _ pats _] ->-                            do t' <- if AssertTotal `elem` opts-                                        then return $ Total []-                                        else calcTotality fc n pats-                               logCoverage 2 $ "Set to " ++ show t'-                               setTotality n t'-                               addIBC (IBCTotal n t')-                               return t'-                        [TyDecl (DCon _ _ _) ty] ->-                            case unApply (getRetTy ty) of-                              (P _ tyn _, _) -> do-                                 let ms = case lookupCtxt tyn (idris_datatypes i) of-                                       [TI _ _ _ _ xs@(_:_)] -> xs-                                       ts -> [tyn]-                                 checkPositive ms (n, ty)-                              _-> return $ Total []-                        _ -> return $ Total []-                x -> return x-        case t' of-            Total _ -> return t'-            Productive -> return t'-            e -> do w <- cmdOptType WarnPartial-                    if TotalFn `elem` opts-                       then do totalityError t'; return t'-                       else do when (w && not (PartialFn `elem` opts)) $-                                   warnPartial n t'-                               return t'-  where-    totalityError t = do i <- getIState-                         let msg = show n ++ " is " ++ show t-                         putIState i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i}-                         addIBC (IBCTotCheckErr fc msg)--    warnPartial n t-       = do i <- getIState-            case lookupDef n (tt_ctxt i) of-               [x] -> do-                  iWarn fc . pprintErr i . Msg $ "Warning - " ++ show n ++ " is " ++ show t---                                ++ "\n" ++ show x---                   let cg = lookupCtxtName Nothing n (idris_callgraph i)---                   iputStrLn (show cg)---checkDeclTotality :: (FC, Name) -> Idris Totality-checkDeclTotality (fc, n)-    = do logCoverage 2 $ "Checking " ++ show n ++ " for totality"-         i <- getIState-         let opts = case lookupCtxtExact n (idris_flags i) of-                              Just fs -> fs-                              _ -> []-         when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n-         t <- checkTotality [] fc n-         return t---- If the name calls something which is partial, set it as partial-verifyTotality :: (FC, Name) -> Idris ()-verifyTotality (fc, n)-    = do logCoverage 2 $ "Checking " ++ show n ++ "'s descendents are total"-         ist <- getIState-         case lookupTotalExact n (tt_ctxt ist) of-              Just (Total _) -> do-                 let ns = getNames (tt_ctxt ist)--                 case getPartial ist [] ns of-                      Nothing -> return ()-                      Just bad -> do let t' = Partial (Other bad)-                                     logCoverage 2 $ "Set to " ++ show t'-                                     setTotality n t'-                                     addIBC (IBCTotal n t')-              _ -> return ()-  where-    getNames ctxt = case lookupDefExact n ctxt of-                         Just (CaseOp  _ _ _ _ _ defs)-                           -> let (top, def) = cases_compiletime defs in-                                  map fst (findCalls' True def top)-                         _ -> []--    getPartial ist [] [] = Nothing-    getPartial ist bad [] = Just bad-    getPartial ist bad (n : ns)-        = case lookupTotalExact n (tt_ctxt ist) of-               Just (Partial _) -> getPartial ist (n : bad) ns-               _ -> getPartial ist bad ns---- | Calculate the size change graph for this definition------ SCG for a function f consists of a list of:---    (g, [(a1, sizechange1), (a2, sizechange2), ..., (an, sizechangen)])------ where g is a function called--- a1 ... an are the arguments of f in positions 1..n of g--- sizechange1 ... sizechange2 is how their size has changed wrt the input--- to f---    Nothing, if the argument is unrelated to the input-buildSCG :: (FC, Name) -> Idris ()-buildSCG (_, n) = do-   ist <- getIState-   case lookupCtxt n (idris_callgraph ist) of-       [cg] -> case lookupDefExact n (tt_ctxt ist) of-           Just (CaseOp _ _ _ pats _ cd) ->-             let (args, sc) = cases_totcheck cd in-               do logCoverage 2 $ "Building SCG for " ++ show n ++ " from\n"-                                ++ show pats ++ "\n" ++ show sc-                  let newscg = buildSCG' ist n (rights pats) args-                  logCoverage 5 $ "SCG is: " ++ show newscg-                  addToCG n ( cg { scg = newscg } )-           _ -> return () -- CG comes from a type declaration only-       [] -> logCoverage 5 $ "Could not build SCG for " ++ show n ++ "\n"-       x -> error $ "buildSCG: " ++ show (n, x)--delazy = delazy' False -- not lazy codata-delazy' all t@(App _ f a)-     | (P _ (UN l) _, [_, _, arg]) <- unApply t,-       l == txt "Force" = delazy' all arg-     | (P _ (UN l) _, [P _ (UN lty) _, _, arg]) <- unApply t,-       l == txt "Delay" && (all || lty /= txt "Infinite") = delazy arg-     | (P _ (UN l) _, [P _ (UN lty) _, arg]) <- unApply t,-       l == txt "Delayed" && (all || lty /= txt "Infinite") = delazy' all arg-delazy' all (App s f a) = App s (delazy' all f) (delazy' all a)-delazy' all (Bind n b sc) = Bind n (fmap (delazy' all) b) (delazy' all sc)-delazy' all t = t--data Guardedness = Toplevel | Unguarded | Guarded | Delayed-  deriving Show--buildSCG' :: IState -> Name -> [(Term, Term)] -> [Name] -> [SCGEntry]-buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where-  scgPat (lhs, rhs) = let lhs' = delazy lhs-                          rhs' = delazy rhs-                          (f, pargs) = unApply (dePat lhs') in-                            findCalls [] Toplevel (dePat rhs') (patvars lhs')-                                      (zip pargs [0..])--  -- Under a delay, calls are excluded from the graph - if it's a call to a-  -- non-total function we'll find that in the final totality check-  findCalls cases Delayed ap@(P _ n _) pvs args = []-  findCalls cases guarded ap@(App _ f a) pvs pargs-     -- under a call to "assert_total", don't do any checking, just believe-     -- that it is total.-     | (P _ (UN at) _, [_, _]) <- unApply ap,-       at == txt "assert_total" = []-     -- don't go under calls to functions which are asserted total-     | (P _ n _, _) <- unApply ap,-       Just opts <- lookupCtxtExact n (idris_flags ist),-       AssertTotal `elem` opts = []-     -- under a guarded call to "Delay Infinite", we are 'Delayed', so don't-     -- check under guarded constructors.-     | (P _ (UN del) _, [_,_,arg]) <- unApply ap,-       Guarded <- guarded,-       del == txt "Delay"-           = findCalls cases Delayed arg pvs pargs-     | (P _ n _, args) <- unApply ap,-       Delayed <- guarded,-       isConName n (tt_ctxt ist)-           = -- Still under a 'Delay' and constructor guarded, so check-             -- just the arguments to the constructor, remaining Delayed-             concatMap (\x -> findCalls cases guarded x pvs pargs) args-     | (P _ ifthenelse _, [_, _, t, e]) <- unApply ap,-       ifthenelse == sNS (sUN "ifThenElse") ["Bool", "Prelude"]-       -- Continue look inside if...then...else blocks-       -- TODO: Consider whether we should do this for user defined ifThenElse-       -- rather than just the one in the Prelude as a special case-       = findCalls cases guarded t pvs pargs ++-         findCalls cases guarded e pvs pargs-     | (P _ n _, args) <- unApply ap,-       caseName n && n /= topfn,-       notPartial (lookupTotalExact n (tt_ctxt ist))-       -- case block - look inside the block, as long as it was covering-       -- (i.e. not currently set at Partial) to get a more accurate size-       -- change result from the top level patterns (also to help pass-       -- information through from guarded corecursion accurately)-       = concatMap (\x -> findCalls cases Unguarded x pvs pargs) args ++-             if n `notElem` cases-                then findCallsCase (n : cases) guarded n args pvs pargs-                else []-     | (P _ n _, args) <- unApply ap,-       Delayed <- guarded-       -- Under a delayed recursive call just check the arguments-           = concatMap (\x -> findCalls cases Unguarded x pvs pargs) args-     | (P _ n _, args) <- unApply ap-        -- Ordinary call, not under a delay.-        -- If n is a constructor, set 'args' as Guarded-        = let nguarded = case guarded of-                              Unguarded -> Unguarded-                              x -> if isConName n (tt_ctxt ist)-                                      then Guarded-                                      else Unguarded in-              mkChange n args pargs ++-                 concatMap (\x -> findCalls cases nguarded x pvs pargs) args-    where notPartial (Just (Partial NotCovering)) = False-          notPartial _ = True-  findCalls cases guarded (App _ f a) pvs pargs-        = findCalls cases Unguarded f pvs pargs ++ findCalls cases Unguarded a pvs pargs-  findCalls cases guarded (Bind n (Let t v) e) pvs pargs-        = findCalls cases Unguarded t pvs pargs ++-          findCalls cases Unguarded v pvs pargs ++ findCalls cases guarded e (n : pvs) pargs-  findCalls cases guarded (Bind n t e) pvs pargs-        = findCalls cases Unguarded (binderTy t) pvs pargs ++-          findCalls cases guarded e (n : pvs) pargs-  findCalls cases guarded (P _ f _ ) pvs pargs-      | not (f `elem` pvs) = [(f, [])]-  findCalls _ _ _ _ _ = []--  -- Assumption is that names are preserved in the case block (shadowing-  -- dealt with by the elaborator) so we can just assume the top level names-  -- are okay for building the size change-  findCallsCase cases guarded n args pvs pargs-      = case lookupDefExact n (tt_ctxt ist) of-           Just (CaseOp _ _ _ pats _ cd) ->-                concatMap (fccPat cases pvs pargs args guarded) (rights pats)-           Nothing -> []--  fccPat cases pvs pargs args g (lhs, rhs)-      = let lhs' = delazy lhs-            rhs' = delazy rhs-            (f, pargs_case) = unApply (dePat lhs')-            -- pargs is a pair of a term, and the argument position that-            -- term appears in. If any of the arguments to the case block-            -- are also on the lhs, we also want those patterns to appear-            -- in the parg list so that we'll spot patterns which are-            -- smaller than then-            newpargs = newPArg args pargs-            -- Now need to update the rhs of the case with the names in the-            -- outer definition: In rhs', wherever we see what's in pargs_case,-            -- replace it with the corresponding thing in pargs-            csubs = zip pargs_case args-            newrhs = doCaseSubs csubs (dePat rhs')-            pargs' = pargs ++ addPArg newpargs pargs_case in-               findCalls cases g newrhs pvs pargs'-    where-      doCaseSubs [] tm = tm-      doCaseSubs ((x, x') : cs) tm-           = doCaseSubs (subIn x x' cs) (substTerm x x' tm)--      subIn x x' [] = []-      subIn x x' ((l, r) : cs)-          = (substTerm x x' l, substTerm x x' r) : subIn x x' cs--  addPArg (Just (t, i) : ts) (t' : ts') = (t', i) : addPArg ts ts'-  addPArg (Nothing : ts) (t' : ts') = addPArg ts ts'-  addPArg _ _ = []--  newPArg :: [Term] -> [(Term, Int)] -> [Maybe (Term, Int)]-  newPArg (t : ts) pargs = case lookup t pargs of-                                Just i -> Just (t, i) : newPArg ts pargs-                                Nothing -> Nothing : newPArg ts pargs-  newPArg [] pargs = []--  expandToArity n args-     = case lookupTy n (tt_ctxt ist) of-            [ty] -> expand 0 (normalise (tt_ctxt ist) [] ty) args-            _ -> args-     where expand i (Bind n (Pi _ _ _) sc) (x : xs) = x : expand (i + 1) sc xs-           expand i (Bind n (Pi _ _ _) sc) [] = Just (i, Same) : expand (i + 1) sc []-           expand i _ xs = xs--  mkChange n args pargs = [(n, expandToArity n (sizes args))]-    where-      sizes [] = []-      sizes (a : as) = checkSize a pargs : sizes as--      -- find which argument in pargs <a> is smaller than, if any-      checkSize a ((p, i) : ps)-          | a == p = Just (i, Same)-          | (P _ (UN as) _, [_,_,arg,_]) <- unApply a,-            as == txt "assert_smaller" && arg == p-                  = Just (i, Smaller)-          | smaller Nothing a (p, Nothing) = Just (i, Smaller)-          | otherwise = checkSize a ps-      checkSize a [] = Nothing--      -- the smaller thing we find must be defined in the same group of mutally-      -- defined types as <a>, and not be coinductive - so carry the type of-      -- the constructor we've gone under.--      smaller (Just tyn) a (t, Just tyt)-         | a == t = isInductive (fst (unApply (getRetTy tyn)))-                                (fst (unApply (getRetTy tyt)))-      smaller ty a (ap@(App _ f s), _)-          | (P (DCon _ _ _) n _, args) <- unApply ap-               = let tyn = getType n in-                     any (smaller (ty `mplus` Just tyn) a)-                         (zip args (map toJust (getArgTys tyn)))-      -- check higher order recursive arguments-      smaller ty (App _ f s) a = smaller ty f a-      smaller _ _ _ = False--      toJust (n, t) = Just t--      getType n = case lookupTyExact n (tt_ctxt ist) of-                       Just ty -> delazy (normalise (tt_ctxt ist) [] ty) -- must exist--      isInductive (P _ nty _) (P _ nty' _) =-          let (co, muts) = case lookupCtxt nty (idris_datatypes ist) of-                                [TI _ x _ _ muts] -> (x, muts)-                                _ -> (False, []) in-              (nty == nty' || any (== nty') muts) && not co-      isInductive _ _ = False--  dePat (Bind x (PVar ty) sc) = dePat (instantiate (P Bound x ty) sc)-  dePat t = t--  patvars (Bind x (PVar _) sc) = x : patvars sc-  patvars _ = []--checkSizeChange :: Name -> Idris Totality-checkSizeChange n = do-   ist <- getIState-   case lookupCtxt n (idris_callgraph ist) of-       [cg] -> do let ms = mkMultiPaths ist [] (scg cg)-                  logCoverage 5 ("Multipath for " ++ show n ++ ":\n" ++-                            "from " ++ show (scg cg) ++ "\n" ++-                            show (length ms) ++ "\n" ++-                            showSep "\n" (map show ms))-                  logCoverage 6 (show cg)-                  -- every multipath must have an infinitely descending-                  -- thread, then the function terminates-                  -- also need to checks functions called are all total-                  -- (Unchecked is okay as we'll spot problems here)-                  let tot = map (checkMP ist n (getArity ist n)) ms-                  logCoverage 4 $ "Generated " ++ show (length tot) ++ " paths"-                  logCoverage 5 $ "Paths for " ++ show n ++ " yield " ++-                       (showSep "\n" (map show (zip ms tot)))-                  return (noPartial tot)-       [] -> do logCoverage 5 $ "No paths for " ++ show n-                return Unchecked-  where getArity ist n-          = case lookupTy n (tt_ctxt ist) of-                 [ty] -> arity (normalise (tt_ctxt ist) [] ty)-                 _ -> error "Can't happen: checkSizeChange.getArity"--type MultiPath = [SCGEntry]--mkMultiPaths :: IState -> MultiPath -> [SCGEntry] -> [MultiPath]-mkMultiPaths ist path [] = [reverse path]-mkMultiPaths ist path cg = concatMap extend cg-  where extend (nextf, args)-           | (nextf, args) `inPath` path = [ reverse ((nextf, args) : path) ]-           | [Unchecked] <- lookupTotal nextf (tt_ctxt ist)-               = case lookupCtxt nextf (idris_callgraph ist) of-                    [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)-                    _ -> [ reverse ((nextf, args) : path) ]-           | otherwise = [ reverse ((nextf, args) : path) ]--        inPath :: SCGEntry -> [SCGEntry] -> Bool-        inPath f [] = False-        inPath f (g : gs) = smallerEq f g || f == g || inPath f gs--        smallerEq :: SCGEntry -> SCGEntry -> Bool-        smallerEq (f, args) (g, args')-            = f == g && not (null (filter smallers args))-                     && filter smallers args == filter smallers args'-        smallers (Just (_, Smaller)) = True-        smallers _ = False---- If any route along the multipath leads to infinite descent, we're fine.--- Try a route beginning with every argument.---   If we reach a point we've been to before, but with a smaller value,---   that means there is an infinitely descending path from that argument.--checkMP :: IState -> Name -> Int -> MultiPath -> Totality-checkMP ist topfn i mp = if i > 0-                     then let paths = (map (tryPath 0 [] mp) [0..i-1]) in---                               trace ("Paths " ++ show paths) $-                               collapse paths-                     else tryPath 0 [] mp 0-  where-    tryPath' d path mp arg-           = let res = tryPath d path mp arg in-                 trace (show mp ++ "\n" ++ show arg ++ " " ++ show res) res--    mkBig (e, d) = (e, 10000)--    tryPath :: Int -> [((SCGEntry, Int), Int)] -> MultiPath -> Int -> Totality-    tryPath desc path [] _ = Total []---     tryPath desc path ((UN "believe_me", _) : _) arg---             = Partial BelieveMe-    -- if we get to a constructor, it's fine as long as it's strictly positive-    tryPath desc path ((f, _) : es) arg-        | [TyDecl (DCon _ _ _) _] <- lookupDef f (tt_ctxt ist)-            = case lookupTotalExact f (tt_ctxt ist) of-                   Just (Total _) -> Unchecked -- okay so far-                   Just (Partial _) -> Partial (Other [f])-                   x -> Unchecked -- An error elsewhere, set as Unchecked to make-                                  -- some progress-        | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)-            = Total []-    tryPath desc path (e@(f, args) : es) arg-        | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a-        | e `elem` es && allNothing args = Partial (Mutual [f])-    tryPath desc path (e@(f, nextargs) : es) arg-        | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a-        | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])-        | Just d <- lookup (e, arg) path-            = if desc - d > 0 -- Now lower than when we were last here-                   then -- trace ("Descent " ++ show (desc - d) ++ " "-                        --      ++ show (path, e)) $-                        Total []-                   else Partial (Mutual (map (fst . fst . fst) path ++ [f]))-        | e `elem` map (fst . fst) path-           && not (f `elem` map fst es)-              = Partial (Mutual (map (fst . fst . fst) path ++ [f]))-        | [Unchecked] <- lookupTotal f (tt_ctxt ist) =-            let argspos = zip nextargs [0..]-                pathres =-                  do (a, pos) <- argspos-                     case a of-                        Nothing -> -- gone up, but if the-                                   -- rest definitely terminates without any-                                   -- cycles (including the path so far, which-                                   -- we take as inaccessible) the path is fine-                            return $ tryPath 0 (map mkBig (((e, arg), desc) : path)) es pos-                        Just (nextarg, sc) ->-                          if nextarg == arg then-                            case sc of-                              Same -> return $ tryPath desc (((e, arg), desc) : path)-                                                       es pos-                              Smaller -> return $ tryPath (desc+1)-                                                          (((e, arg), desc) : path)-                                                          es-                                                          pos-                              _ -> trace ("Shouldn't happen " ++ show e) $-                                      return (Partial Itself)-                            else return Unchecked in---                   trace (show (desc, argspos, path, es, pathres)) $-                   collapse pathres--        | otherwise = Unchecked--allNothing :: [Maybe a] -> Bool-allNothing xs = null (collapseNothing (zip xs [0..]))--collapseNothing :: [(Maybe a, b)] -> [(Maybe a, b)]-collapseNothing ((Nothing, t) : xs)-   = (Nothing, t) : filter (\ (x, _) -> case x of-                                             Nothing -> False-                                             _ -> True) xs-collapseNothing (x : xs) = x : collapseNothing xs-collapseNothing [] = []--noPartial :: [Totality] -> Totality-noPartial (Partial p : xs) = Partial p-noPartial (_ : xs)         = noPartial xs-noPartial []               = Total []--collapse :: [Totality] -> Totality-collapse xs = collapse' Unchecked xs-collapse' def (Total r : xs)   = Total r-collapse' def (Unchecked : xs) = collapse' def xs-collapse' def (d : xs)         = collapse' d xs--- collapse' Unchecked []         = Total []-collapse' def []               = def--totalityCheckBlock :: Idris ()-totalityCheckBlock = do-         ist <- getIState-         -- Do totality checking after entire mutual block-         mapM_ (\n -> do logElab 5 $ "Simplifying " ++ show n-                         ctxt' <- do ctxt <- getContext-                                     tclift $ simplifyCasedef n (getErasureInfo ist) ctxt-                         setContext ctxt')-                 (map snd (idris_totcheck ist))-         mapM_ buildSCG (idris_totcheck ist)-         mapM_ checkDeclTotality (idris_totcheck ist)-         clear_totcheck+Description : Clause generation for coverage checking+Copyright   :+License     : BSD3+Maintainer  : The Idris Community.+-}+{-# LANGUAGE PatternGuards #-}+module Idris.Coverage(genClauses, validCoverageCase, recoverableCoverage,+                      mkPatTm) where++import Idris.AbsSyntax+import Idris.Core.CaseTree+import Idris.Core.Evaluate+import Idris.Core.TT+import Idris.Delaborate+import Idris.Error+import Idris.Output (iWarn, iputStrLn)++import Control.Monad.State.Strict+import Data.Char+import Data.Either+import Data.List+import Data.Maybe+import Debug.Trace++-- | Generate a pattern from an 'impossible' LHS.+--+-- We need this to eliminate the pattern clauses which have been+-- provided explicitly from new clause generation.+mkPatTm :: PTerm -> Idris Term+mkPatTm t = do i <- getIState+               let timp = addImpl' True [] [] [] i t+               evalStateT (toTT (mapPT deNS timp)) 0+  where+    toTT (PRef _ _ n) = do i <- lift getIState+                           case lookupNameDef n (tt_ctxt i) of+                                [(n', TyDecl nt _)] -> return $ P nt n' Erased+                                _ -> return $ P Ref n Erased+    toTT (PApp _ t args) = do t' <- toTT t+                              args' <- mapM (toTT . getTm) args+                              return $ mkApp t' args'+    toTT (PDPair _ _ _ l _ r) = do l' <- toTT l+                                   r' <- toTT r+                                   return $ mkApp (P Ref sigmaCon Erased) [Erased, Erased, l', r']+    toTT (PPair _ _ _ l r) = do l' <- toTT l+                                r' <- toTT r+                                return $ mkApp (P Ref pairCon Erased) [Erased, Erased, l', r']+    -- For alternatives, pick the first and drop the namespaces. It doesn't+    -- really matter which is taken since matching will ignore the namespace.+    toTT (PAlternative _ _ (a : as)) = toTT a+    toTT _ = do v <- get+                put (v + 1)+                return (P Bound (sMN v "imp") Erased)++    deNS (PRef f hl (NS n _)) = PRef f hl n+    deNS t = t++-- | Given a list of LHSs, generate a extra clauses which cover the remaining+-- cases. The ones which haven't been provided are marked 'absurd' so+-- that the checker will make sure they can't happen.+--+-- This will only work after the given clauses have been typechecked and the+-- names are fully explicit!+genClauses :: FC -> Name -> [([Name], Term)] -> -- (Argument names, LHS) +              [PTerm] -> Idris [PTerm]+-- No clauses (only valid via elab reflection). We should probably still do+-- a check here somehow, e.g. that one of the arguments is an obviously+-- empty type. In practice, this should only really be used for Void elimination.+genClauses fc n lhs_tms [] = return [] +genClauses fc n lhs_tms given+   = do i <- getIState+      +        let lhs_given = zipWith removePlaceholders lhs_tms +                            (map (stripUnmatchable i) (map flattenArgs given))+        +        logCoverage 5 $ "Building coverage tree for:\n" ++ showSep "\n" (map show (lhs_given))+        let givenpos = mergePos (map getGivenPos given)++        (cns, ctree_in) <- +                         case simpleCase False (UnmatchedCase "Undefined") False+                              (CoverageCheck givenpos) emptyFC [] []+                              lhs_given +                              (const []) of+                           OK (CaseDef cns ctree_in _) ->+                              return (cns, ctree_in)+                           Error e -> tclift $ tfail $ At fc e+            +        let ctree = trimOverlapping (addMissingCons i ctree_in)+        let (coveredas, missingas) = mkNewClauses (tt_ctxt i) n cns ctree+        let covered = map (\t -> delab' i t True True) coveredas+        let missing = filter (\x -> x `notElem` covered) $+                          map (\t -> delab' i t True True) missingas++        logCoverage 5 $ "Coverage from case tree for " ++ show n ++ ": " ++ show ctree+        logCoverage 2 $ show (length missing) ++ " missing clauses for " ++ show n+        logCoverage 3 $ "Missing clauses:\n" ++ showSep "\n" +                              (map showTmImpls missing)+        logCoverage 10 $ "Covered clauses:\n" ++ showSep "\n" +                              (map showTmImpls covered)+        return missing+    where+        flattenArgs (PApp fc (PApp _ f as) as')+             = flattenArgs (PApp fc f (as ++ as'))+        flattenArgs t = t++getGivenPos :: PTerm -> [Int]+getGivenPos (PApp _ _ pargs) = getGiven 0 (map getTm pargs)+  where+    getGiven i (Placeholder : tms) = getGiven (i + 1) tms+    getGiven i (_ : tms) = i : getGiven (i + 1) tms+    getGiven i [] = []+getGivenPos _ = []++-- Return a list of Ints which are in every list+mergePos :: [[Int]] -> [Int]+mergePos [] = []+mergePos [x] = x+mergePos (x : xs) = intersect x (mergePos xs)++removePlaceholders :: ([Name], Term) -> PTerm -> ([Name], Term, Term)+removePlaceholders (ns, tm) ptm = (ns, rp tm ptm, Erased)+  where+    rp Erased Placeholder = Erased+    rp tm Placeholder = Inferred tm+    rp tm (PApp _ pf pargs)+       | (tf, targs) <- unApply tm+           = let tf' = rp tf pf+                 targs' = zipWith rp targs (map getTm pargs) in+                 mkApp tf' targs'+    rp tm (PPair _ _ _ pl pr)+       | (tf, [tyl, tyr, tl, tr]) <- unApply tm+           = let tl' = rp tl pl+                 tr' = rp tr pr in+                 mkApp tf [Erased, Erased, tl', tr'] +    rp tm (PDPair _ _ _ pl pt pr)+       | (tf, [tyl, tyr, tl, tr]) <- unApply tm+           = let tl' = rp tl pl+                 tr' = rp tr pr in+                 mkApp tf [Erased, Erased, tl', tr'] +    rp tm _ = tm++mkNewClauses :: Context -> Name -> [Name] -> SC -> ([Term], [Term])+mkNewClauses ctxt fn ns sc +     = (map (mkPlApp (P Ref fn Erased)) $+            mkFromSC True (map (\n -> P Ref n Erased) ns) sc,+        map (mkPlApp (P Ref fn Erased)) $+            mkFromSC False (map (\n -> P Ref n Erased) ns) sc)+  where+    mkPlApp f args = mkApp f (map erasePs args)++    erasePs ap@(App t f a) +        | (f, args) <- unApply ap = mkApp f (map erasePs args)+    erasePs (P _ n _) | not (isConName n ctxt) = Erased+    erasePs tm = tm++    mkFromSC cov args sc = evalState (mkFromSC' cov args sc) []++    mkFromSC' :: Bool -> [Term] -> SC -> State [[Term]] [[Term]]+    mkFromSC' cov args (STerm _) +        = if cov then return [args] else return [] -- leaf of provided case+    mkFromSC' cov args (UnmatchedCase _) +        = if cov then return [] else return [args] -- leaf of missing case+    mkFromSC' cov args ImpossibleCase = return []+    mkFromSC' cov args (Case _ x alts)+       = do done <- get+            if (args `elem` done)+               then return []+               else do alts' <- mapM (mkFromAlt cov args x) alts +                       put (args : done)+                       return (concat alts')+    mkFromSC' cov args _ = return [] -- Should never happen++    mkFromAlt :: Bool -> [Term] -> Name -> CaseAlt -> State [[Term]] [[Term]]+    mkFromAlt cov args x (ConCase c t conargs sc)+       = let argrep = mkApp (P (DCon t (length args) False) c Erased)+                            (map (\n -> P Ref n Erased) conargs)+             args' = map (subst x argrep) args in+             mkFromSC' cov args' sc+    mkFromAlt cov args x (ConstCase c sc)+       = let argrep = Constant c +             args' = map (subst x argrep) args in+             mkFromSC' cov args' sc+    mkFromAlt cov args x (DefaultCase sc)+       = mkFromSC' cov args sc+    mkFromAlt cov _ _ _ = return []++-- Modify the generated case tree (the case tree builder doesn't have access+-- to the context, so can't do this itself).+-- Replaces any missing cases with explicit cases for the missing constructors+addMissingCons :: IState -> SC -> SC+addMissingCons ist sc = evalState (addMissingConsSt ist sc) 0++addMissingConsSt :: IState -> SC -> State Int SC+addMissingConsSt ist (Case t n alts) = liftM (Case t n) (addMissingAlts n alts)+  where+    addMissingAlt :: CaseAlt -> State Int CaseAlt+    addMissingAlt (ConCase n i ns sc) +         = liftM (ConCase n i ns) (addMissingConsSt ist sc)+    addMissingAlt (FnCase n ns sc) +         = liftM (FnCase n ns) (addMissingConsSt ist sc)+    addMissingAlt (ConstCase c sc) +         = liftM (ConstCase c) (addMissingConsSt ist sc)+    addMissingAlt (SucCase n sc) +         = liftM (SucCase n) (addMissingConsSt ist sc)+    addMissingAlt (DefaultCase sc) +         = liftM DefaultCase (addMissingConsSt ist sc)++    addMissingAlts argn as +--          | any hasDefault as = map addMissingAlt as+         | cons@(n:_) <- mapMaybe collectCons as,+           Just tyn <- getConType n,+           Just ti <- lookupCtxtExact tyn (idris_datatypes ist)+             -- If we've fallen through on this argument earlier, then the+             -- things which were matched in other cases earlier can't be missing+             -- cases now+             = let missing = con_names ti \\ cons in+                   do as' <- addCases missing as+                      mapM addMissingAlt as'+         | consts@(n:_) <- mapMaybe collectConsts as+             = let missing = nub (map nextConst consts) \\ consts in+                   mapM addMissingAlt (addCons missing as)+    addMissingAlts n as = mapM addMissingAlt as++    addCases missing [] = return []+    addCases missing (DefaultCase rhs : rest)+       = do missing' <- mapM (genMissingAlt rhs) missing+            return (mapMaybe id missing' ++ rest)+    addCases missing (c : rest) +       = liftM (c :) $ addCases missing rest++    addCons missing [] = []+    addCons missing (DefaultCase rhs : rest)+       = map (genMissingConAlt rhs) missing ++ rest+    addCons missing (c : rest) = c : addCons missing rest++    genMissingAlt rhs n+         | Just (TyDecl (DCon tag arity _) ty) <- lookupDefExact n (tt_ctxt ist)+             = do name <- get+                  put (name + arity)+                  let args = map (name +) [0..arity-1]+                  return $ Just $ ConCase n tag (map (\i -> sMN i "m") args) rhs+         | otherwise = return Nothing++    genMissingConAlt rhs n = ConstCase n rhs++    collectCons (ConCase n i args sc) = Just n+    collectCons _ = Nothing++    collectConsts (ConstCase c sc) = Just c+    collectConsts _ = Nothing++    hasDefault (DefaultCase (UnmatchedCase _)) = False+    hasDefault (DefaultCase _) = True+    hasDefault _ = False++    getConType n = do ty <- lookupTyExact n (tt_ctxt ist)+                      case unApply (getRetTy (normalise (tt_ctxt ist) [] ty)) of+                           (P _ tyn _, _) -> Just tyn+                           _ -> Nothing+    +    -- for every constant in a term (at any level) take next one to make sure+    -- that constants which are not explicitly handled are covered+    nextConst (I c) = I (c + 1)+    nextConst (BI c) = BI (c + 1)+    nextConst (Fl c) = Fl (c + 1)+    nextConst (B8 c) = B8 (c + 1)+    nextConst (B16 c) = B16 (c + 1)+    nextConst (B32 c) = B32 (c + 1)+    nextConst (B64 c) = B64 (c + 1)+    nextConst (Ch c) = Ch (chr $ ord c + 1)+    nextConst (Str c) = Str (c ++ "'")+    nextConst o = o++addMissingConsSt ist sc = return sc++trimOverlapping :: SC -> SC+trimOverlapping sc = trim [] [] sc+  where+    trim :: [(Name, (Name, [Name]))] -> -- Variable - constructor+args already matched+            [(Name, [Name])] -> -- Variable - constructors which it can't be+            SC -> SC+    trim mustbes nots (Case t vn alts)+       | Just (c, args) <- lookup vn mustbes+            = Case t vn (trimAlts mustbes nots vn (substMatch (c, args) alts))+       | Just cantbe <- lookup vn nots+            = let alts' = filter (notConMatch cantbe) alts in+                  Case t vn (trimAlts mustbes nots vn alts')+       | otherwise = Case t vn (trimAlts mustbes nots vn alts)+    trim cs nots sc = sc++    trimAlts cs nots vn [] = []+    trimAlts cs nots vn (ConCase cn t args sc : rest)+        = ConCase cn t args (trim (addMatch vn (cn, args) cs) nots sc) :+            trimAlts cs (addCantBe vn cn nots) vn rest+    trimAlts cs nots vn (FnCase n ns sc : rest)+        = FnCase n ns (trim cs nots sc) : trimAlts cs nots vn rest+    trimAlts cs nots vn (ConstCase c sc : rest)+        = ConstCase c (trim cs nots sc) : trimAlts cs nots vn rest+    trimAlts cs nots vn (SucCase n sc : rest)+        = SucCase n (trim cs nots sc) : trimAlts cs nots vn rest+    trimAlts cs nots vn (DefaultCase sc : rest)+        = DefaultCase (trim cs nots sc) : trimAlts cs nots vn rest++    isConMatch c (ConCase cn t args sc) = c == cn+    isConMatch _ _ = False++    substMatch :: (Name, [Name]) -> [CaseAlt] -> [CaseAlt]+    substMatch ca [] = []+    substMatch (c,args) (ConCase cn t args' sc : _)+        | c == cn = [ConCase c t args (substNames (zip args' args) sc)]+    substMatch ca (_:cs) = substMatch ca cs++    substNames [] sc = sc+    substNames ((n, n') : ns) sc +       = substNames ns (substSC n n' sc)++    notConMatch cs (ConCase cn t args sc) = cn `notElem` cs+    notConMatch cs _ = True++    addMatch vn cn cs = (vn, cn) : cs++    addCantBe :: Name -> Name -> [(Name, [Name])] -> [(Name, [Name])]+    addCantBe vn cn [] = [(vn, [cn])]+    addCantBe vn cn ((n, cbs) : nots)+          | vn == n = ((n, nub (cn : cbs)) : nots)+          | otherwise = ((n, cbs) : addCantBe vn cn nots)++-- | Does this error result rule out a case as valid when coverage checking?+validCoverageCase :: Context -> Err -> Bool+validCoverageCase ctxt (CantUnify _ (topx, _) (topy, _) e _ _)+    = let topx' = normalise ctxt [] topx+          topy' = normalise ctxt [] topy in+          not (sameFam topx' topy' || not (validCoverageCase ctxt e))+  where sameFam topx topy+            = case (unApply topx, unApply topy) of+                   ((P _ x _, _), (P _ y _, _)) -> x == y+                   _ -> False+validCoverageCase ctxt (InfiniteUnify _ _ _) = False+validCoverageCase ctxt (CantConvert _ _ _) = False+validCoverageCase ctxt (At _ e) = validCoverageCase ctxt e+validCoverageCase ctxt (Elaborating _ _ _ e) = validCoverageCase ctxt e+validCoverageCase ctxt (ElaboratingArg _ _ _ e) = validCoverageCase ctxt e+validCoverageCase ctxt _ = True++-- | Check whether an error is recoverable in the sense needed for+-- coverage checking.+recoverableCoverage :: Context -> Err -> Bool+recoverableCoverage ctxt (CantUnify r (topx, _) (topy, _) e _ _)+    = let topx' = normalise ctxt [] topx+          topy' = normalise ctxt [] topy in+          checkRec topx' topy'+  where -- different notion of recoverable than in unification, since we+        -- have no metavars -- just looking to see if a constructor is failing+        -- to unify with a function that may be reduced later+        checkRec (App _ f a) p@(P _ _ _) = checkRec f p+        checkRec p@(P _ _ _) (App _ f a) = checkRec p f+        checkRec fa@(App _ _ _) fa'@(App _ _ _)+            | (f, as) <- unApply fa,+              (f', as') <- unApply fa'+                 = if (length as /= length as')+                      then checkRec f f'+                      else checkRec f f' && and (zipWith checkRec as as')+        checkRec (P xt x _) (P yt y _) = x == y || ntRec xt yt+        checkRec _ _ = False++        ntRec x y | Ref <- x = True+                  | Ref <- y = True+                  | (Bound, Bound) <- (x, y) = True+                  | otherwise = False -- name is different, unrecoverable+recoverableCoverage ctxt (At _ e) = recoverableCoverage ctxt e+recoverableCoverage ctxt (Elaborating _ _ _ e) = recoverableCoverage ctxt e+recoverableCoverage ctxt (ElaboratingArg _ _ _ e) = recoverableCoverage ctxt e+recoverableCoverage _ _ = False+

@@ -10,14 +10,12 @@  module Idris.DSL where -import Data.Generics.Uniplate.Data (transform)- import Idris.AbsSyntax--import Idris.Core.TT import Idris.Core.Evaluate+import Idris.Core.TT  import Control.Monad.State.Strict+import Data.Generics.Uniplate.Data (transform) import Debug.Trace  debindApp :: SyntaxInfo -> PTerm -> PTerm

@@ -12,20 +12,20 @@   , module Idris.Core.DeepSeq   ) where -import Idris.Core.DeepSeq-import Idris.Docstrings-import Idris.Core.TT import Idris.AbsSyntaxTree import Idris.Colours+import Idris.Core.DeepSeq+import Idris.Core.TT+import Idris.Docstrings+import qualified Idris.Docstrings as D+import IRTS.CodegenCommon (OutputType(..)) import IRTS.Lang (PrimFn(..))-import IRTS.CodegenCommon (OutputType (..))-import Util.DynamicLinker -import Control.DeepSeq-import Network.Socket(PortNumber)+import Util.DynamicLinker  import qualified Cheapskate.Types as CT-import qualified Idris.Docstrings as D+import Control.DeepSeq+import Network.Socket (PortNumber)  -- These types don't have Generic instances instance NFData CT.Options where

@@ -13,23 +13,22 @@   , pprintDelabTy, pprintErr, resugar   ) where -import Util.Pretty- import Idris.AbsSyntax-import Idris.Core.TT import Idris.Core.Evaluate-import Idris.Docstrings (overview, renderDocstring, renderDocTerm)+import Idris.Core.TT+import Idris.Docstrings (overview, renderDocTerm, renderDocstring) import Idris.ErrReverse +import Util.Pretty+ import Prelude hiding ((<$>)) +import Control.Applicative (Alternative((<|>)))+import Control.Monad.State import Data.Generics.Uniplate.Data (transform)-import Data.Maybe (mapMaybe) import Data.List (intersperse, nub)+import Data.Maybe (mapMaybe) import qualified Data.Text as T-import Control.Applicative (Alternative((<|>)))-import Control.Monad.State- import Debug.Trace  bugaddr = "https://github.com/idris-lang/Idris-dev/issues"@@ -81,10 +80,10 @@  -- | Delaborate a term without resugaring delab :: IState -> Term -> PTerm-delab i tm = delab' i tm False False +delab i tm = delab' i tm False False  delabMV :: IState -> Term -> PTerm-delabMV i tm = delab' i tm False True +delabMV i tm = delab' i tm False True  -- | Delaborate a term directly, leaving case applications as they are. -- We need this for interactive case splitting, where we need access to the@@ -112,7 +111,7 @@ delabTy' ist imps tm fullname mvs docases = de [] imps tm   where     un = fileFC "(val)"-    +     -- Special case for spotting applications of case functions     -- (Normally the scrutinee is let-bound, but hole types get normalised,     -- so they could appear in this form. The scrutinee is always added as@@ -123,7 +122,7 @@           | docases           , isCaseApp sc           , (P _ cOp _, args@(_:_)) <- unApply sc-          , Just caseblock <- delabCase env imps (last args) cOp args +          , Just caseblock <- delabCase env imps (last args) cOp args                  = caseblock      de env _ (App _ f a) = deFn env f [a]@@ -174,6 +173,7 @@     de env _ (Proj _ _) = error "Delaboration got run-time-only Proj!"     de env _ Erased = Placeholder     de env _ Impossible = Placeholder+    de env _ (Inferred t) = Placeholder     de env _ (TType i) = PType un     de env _ (UType u) = PUniverse un u 

@@ -9,11 +9,10 @@  import Idris.AbsSyntax import Idris.ASTUtils-import Idris.Imports-import Idris.Output (sendHighlighting)- import Idris.Core.Evaluate import Idris.Core.TT+import Idris.Imports+import Idris.Output (sendHighlighting)  import Util.DynamicLinker 

@@ -5,7 +5,7 @@ License     : BSD3 Maintainer  : The Idris Community. -}-{-# LANGUAGE DeriveFunctor, PatternGuards, MultiWayIf #-}+{-# LANGUAGE DeriveFunctor, MultiWayIf, PatternGuards #-} {-# OPTIONS_GHC -fwarn-incomplete-patterns #-} module Idris.Docs (     pprintDocs@@ -15,19 +15,20 @@  import Idris.AbsSyntax import Idris.AbsSyntaxTree-import Idris.Delaborate-import Idris.Core.TT import Idris.Core.Evaluate-import Idris.Docstrings (Docstring, emptyDocstring, noDocs, nullDocstring, renderDocstring, DocTerm, renderDocTerm, overview)+import Idris.Core.TT+import Idris.Delaborate+import Idris.Docstrings (DocTerm, Docstring, emptyDocstring, noDocs,+                         nullDocstring, overview, renderDocTerm,+                         renderDocstring)  import Util.Pretty  import Prelude hiding ((<$>))  import Control.Arrow (first)--import Data.Maybe import Data.List+import Data.Maybe import qualified Data.Text as T  -- TODO: Only include names with public/export accessibility@@ -48,6 +49,7 @@              | InterfaceDoc Name d  -- interface docs                             [FunDoc' d] -- method docs                             [(Name, Maybe d)] -- parameters and their docstrings+                            [PTerm] -- parameter constraints                             [(Maybe Name, PTerm, (d, [(Name, d)]))] -- implementations: name for named implementations, the constraint term, the docs                             [PTerm] -- sub interfaces                             [PTerm] -- super interfaces@@ -139,13 +141,18 @@              if null args then text "No constructors."              else nest 4 (text "Constructors:" <> line <>                           vsep (map (pprintFDWithoutTotality ist False) args))-pprintDocs ist (InterfaceDoc n doc meths params implementations sub_interfaces super_interfaces ctor)+pprintDocs ist (InterfaceDoc n doc meths params constraints implementations sub_interfaces super_interfaces ctor)            = nest 4 (text "Interface" <+> prettyName True (ppopt_impl ppo) [] n <>                      if nullDocstring doc                        then empty                        else line <> renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc)              <> line <$>              nest 4 (text "Parameters:" <$> prettyParameters)++             <> (if null constraints+                 then empty+                 else line <$> nest 4 (text "Constraints:" <$> prettyConstraints))+              <> line <$>              nest 4 (text "Methods:" <$>                       vsep (map (pprintFDWithTotality ist False) meths))@@ -232,6 +239,9 @@     isSubInterface (PPi _   _            _ _ pt)                                           = isSubInterface pt     isSubInterface _                                                                       = False +    prettyConstraints =+      cat (punctuate (comma <> space) (map (pprintPTerm ppo params' [] infixes) constraints))+     prettyParameters =       if any (isJust . snd) params          then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)@@ -335,7 +345,7 @@                      SN _ -> return Nothing                      _    -> fmap Just $ docFun ctorN        return $ InterfaceDoc-                  n docstr mdocs params+                  n docstr mdocs params (interface_constraints ci)                   implementations' (map (\(_,tm,_) -> tm) sub_interfaces) super_interfaces                   ctorDocs   where

@@ -14,24 +14,21 @@   , renderHtml, annotCode, DocTerm(..), renderDocTerm, checkDocstring   ) where -import qualified Cheapskate as C-import qualified Cheapskate.Types as CT-import Cheapskate.Html (renderDoc)+import Idris.Core.TT (Err, Name, OutputAnnotation(..), Term, TextFormatting(..))  import Util.Pretty -import Idris.Core.TT (OutputAnnotation(..), TextFormatting(..), Name, Term, Err)- import Prelude hiding ((<$>)) -import qualified Data.Text as T-import qualified Data.Foldable as F+import qualified Cheapskate as C+import Cheapskate.Html (renderDoc)+import qualified Cheapskate.Types as CT import Data.Foldable (Foldable)-import Data.Traversable (Traversable)+import qualified Data.Foldable as F import qualified Data.Sequence as S-+import qualified Data.Text as T+import Data.Traversable (Traversable) import GHC.Generics (Generic)- import Text.Blaze.Html (Html)  -- | The various kinds of code samples that can be embedded in docs

@@ -7,12 +7,11 @@ -} module Idris.Elab.AsPat(desugarAs) where -import Idris.Core.TT import Idris.AbsSyntax+import Idris.Core.TT  import Control.Applicative import Control.Monad.State.Strict- import Data.Generics.Uniplate.Data (transformM)  -- | Desugar by changing x@y on lhs to let x = y in ... or rhs

@@ -10,58 +10,54 @@  import Idris.AbsSyntax import Idris.ASTUtils+import Idris.Core.CaseTree+import Idris.Core.Elaborate hiding (Tactic(..))+import Idris.Core.Evaluate+import Idris.Core.Execute+import Idris.Core.TT+import Idris.Core.Typecheck+import Idris.Coverage+import Idris.DataOpts+import Idris.DeepSeq+import Idris.Delaborate+import Idris.Docstrings hiding (Unchecked) import Idris.DSL+import Idris.Elab.AsPat+import Idris.Elab.Term+import Idris.Elab.Transform+import Idris.Elab.Type+import Idris.Elab.Utils import Idris.Error-import Idris.Delaborate import Idris.Imports-import Idris.Elab.Term-import Idris.Coverage-import Idris.DataOpts-import Idris.Providers-import Idris.Primitives import Idris.Inliner+import Idris.Output (iRenderResult, iWarn, iputStrLn, pshow, sendHighlighting) import Idris.PartialEval+import Idris.Primitives+import Idris.Providers+import Idris.Termination import Idris.Transforms-import Idris.DeepSeq-import Idris.Output (iputStrLn, pshow, iWarn, iRenderResult, sendHighlighting) import IRTS.Lang -import Idris.Elab.AsPat-import Idris.Elab.Type-import Idris.Elab.Transform-import Idris.Elab.Utils--import Idris.Core.TT-import Idris.Core.Elaborate hiding (Tactic(..))-import Idris.Core.Evaluate-import Idris.Core.Execute-import Idris.Core.Typecheck-import Idris.Core.CaseTree--import Idris.Docstrings hiding (Unchecked) import Util.Pretty hiding ((<$>))+import Util.Pretty (pretty, text)  import Prelude hiding (id, (.))-import Control.Category  import Control.Applicative hiding (Const)+import Control.Category import Control.DeepSeq import Control.Monad-import Control.Monad.State.Strict as State import qualified Control.Monad.State.Lazy as LState+import Control.Monad.State.Strict as State+import Data.Char (isLetter, toLower) import Data.List-import Data.Maybe-import Data.Word--import Debug.Trace-+import Data.List.Split (splitOn) import qualified Data.Map as Map+import Data.Maybe import qualified Data.Set as S import qualified Data.Text as T-import Data.Char(isLetter, toLower)-import Data.List.Split (splitOn)--import Util.Pretty(pretty, text)+import Data.Word+import Debug.Trace import Numeric  -- | Elaborate a collection of left-hand and right-hand pairs - that is, a@@ -91,11 +87,16 @@            cs_elab <- mapM (elabClause info opts)                            (zip [0..] cs)            ctxt <- getContext-           -- pats_raw is the version we'll work with at compile time:-           -- no simplification or PE+           -- pats_raw is the basic type checked version, no PE or forcing+           let optinfo = idris_optimisation ist            let (pats_in, cs_full) = unzip cs_elab            let pats_raw = map (simple_lhs ctxt) pats_in+           -- We'll apply forcing to the left hand side here, so that we don't+           -- do any unnecessary case splits+           let pats_forced = map (force_lhs optinfo) pats_raw+            logElab 3 $ "Elaborated patterns:\n" ++ show pats_raw+           logElab 5 $ "Forced patterns:\n" ++ show pats_forced             solveDeferred fc n @@ -114,9 +115,10 @@            -- If the definition is specialisable, this reduces the            -- RHS            pe_tm <- doPartialEval ist tpats+            let pats_pe = if petrans-                            then map (simple_lhs ctxt) pe_tm-                            else pats_raw+                            then map (force_lhs optinfo . simple_lhs ctxt) pe_tm+                            else pats_forced             let tcase = opt_typecase (idris_options ist) @@ -143,11 +145,19 @@             -- addCaseDef builds case trees from <pdef> and <pdef'> -           -- pdef is the compile-time pattern definition.-           -- This will get further inlined to help with totality checking.-           let pdef = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) $ map debind pats_raw+           -- pdef is the compile-time pattern definition, after forcing+           -- optimisation applied to LHS+           let pdef = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) $ +                          map debind pats_forced+           -- pdef_cov is the pattern definition without forcing, which+           -- we feed to the coverage checker (we need to know what the+           -- programmer wrote before forcing erasure)+           let pdef_cov+                    = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) $ +                          map debind pats_raw            -- pdef_pe is the one which will get further optimised-           -- for run-time, and, partially evaluated+           -- for run-time, with no forcing optimisation of the LHS because+           -- the affects erasure. Also, it's partially evaluated            let pdef_pe = map debind pats_transformed             logElab 5 $ "Initial typechecked patterns:\n" ++ show pats_raw@@ -176,13 +186,15 @@            pmissing <-                    if cov && not (hasDefault pats_raw)                       then do -- Generate clauses from the given possible cases-                              missing <- genClauses fc n (map getLHS pdef) cs_full+                              missing <- genClauses fc n +                                                 (map (\ (ns,tm,_) -> (ns, tm)) pdef)+                                                 cs_full                               -- missing <- genMissing n scargs sc-                              missing' <- filterM (checkPossible info fc True n) missing+                              missing' <- checkPossibles info fc True n missing                               -- Filter out the ones which match one of the                               -- given cases (including impossible ones)                               let clhs = map getLHS pdef-                              logElab 2 $ "Must be unreachable:\n" +++                              logElab 2 $ "Must be unreachable (" ++ show (length missing') ++ "):\n" ++                                           showSep "\n" (map showTmImpls missing') ++                                          "\nAgainst: " ++                                           showSep "\n" (map (\t -> showTmImpls (delab ist t)) (map getLHS pdef))@@ -191,7 +203,7 @@                               -- unification may force a variable to take a                               -- particular form, rather than force a case                               -- to be impossible.-                              return (filter (noMatch ist clhs) missing')+                              return missing' -- (filter (noMatch ist clhs) missing')                       else return []            let pcover = null pmissing @@ -233,6 +245,7 @@            putIState (ist { idris_patdefs = addDef n (force pdef_pe, force pmissing)                                                 (idris_patdefs ist) })            let caseInfo = CaseInfo (inlinable opts) (inlinable opts) (dictionary opts)+            case lookupTyExact n ctxt of                Just ty ->                    do ctxt' <- do ctxt <- getContext@@ -243,10 +256,8 @@                                                    (AssertTotal `elem` opts)                                                    atys                                                    inacc-                                                   pats_pe+                                                   pats_forced                                                    pdef-                                                   pdef -- compile time-                                                   pdef_inl -- inlined                                                    pdef' ty                                                    ctxt                       setContext ctxt'@@ -282,6 +293,19 @@            -- all called functions, and fail if any of them are also            -- 'Partial NotCovering'            when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n+           -- Add the 'AllGuarded' flag if it's guaranteed that every+           -- 'Inf' argument will be guarded by constructors in the result+           -- (allows productivity check to go under this function)+           checkIfGuarded n+           -- If this has %static arguments, cache the names of functions+           -- it calls for partial evaluation later+           ist <- getIState+           let statics = case lookupCtxtExact n (idris_statics ist) of+                              Just ns -> ns+                              Nothing -> []+           when (or statics) $ do getAllNames n+                                  return ()+   where     noMatch i cs tm = all (\x -> case trim_matchClause i (delab' i x True True) tm of                                       Right _ -> False@@ -323,9 +347,13 @@      -- Simplify the left hand side of a definition, to remove any lets     -- that may have arisen during elaboration-    simple_lhs ctxt (Right (x, y)) = Right (Idris.Core.Evaluate.simplify ctxt [] x, y)+    simple_lhs ctxt (Right (x, y)) +        = Right (Idris.Core.Evaluate.simplify ctxt [] x, y)     simple_lhs ctxt t = t +    force_lhs opts (Right (x, y)) = Right (forceWith opts x, y)+    force_lhs opts t = t+     simple_rt ctxt (p, x, y) = (p, x, force (uniqueBinders p                                                 (rt_simplify ctxt [] y))) @@ -348,6 +376,28 @@                                 Just t -> return t                                 Nothing -> ierror (At fc (Msg "No specialisation achieved")) +forceWith :: Ctxt OptInfo -> Term -> Term+forceWith opts lhs = -- trace (show lhs ++ "\n==>\n" ++ show (force lhs) ++ "\n----") $+                      force lhs+  where+    -- If there's forced arguments, erase them+    force ap@(App _ _ _)+       | (fn@(P _ c _), args) <- unApply ap,+         Just copt <- lookupCtxtExact c opts+            = let args' = eraseArg 0 (forceable copt) args in+                  mkApp fn (map force args')+    force (App t f a)+       = App t (force f) (force a)+    -- We might have pat bindings, so go under them+    force (Bind n b sc) = Bind n b (force sc)+    -- Everything else, leave it alone+    force t = t++    eraseArg i fs (n : ns) | i `elem` fs = Erased : eraseArg (i + 1) fs ns+                           | otherwise = n : eraseArg (i + 1) fs ns+    eraseArg i _ [] = []++ -- | Find 'static' applications in a term and partially evaluate them. -- Return any new transformation rules elabPE :: ElabInfo -> FC -> Name -> Term -> Idris [(Term, Term)]@@ -376,8 +426,8 @@     mkSpecialised specapp_in = do         ist <- getIState         ctxt <- getContext-        let (specTy, specapp) = getSpecTy ist specapp_in-        let (n, newnm, specdecl) = getSpecClause ist specapp+        (specTy, specapp) <- getSpecTy ist specapp_in+        let (n, newnm, specdecl) = getSpecClause ist specapp specTy         let lhs = pe_app specdecl         let rhs = pe_def specdecl         let undef = case lookupDefExact newnm ctxt of@@ -404,21 +454,22 @@                 let opts = [Specialise ((if pe_simple specdecl                                             then map (\x -> (x, Nothing)) cgns'                                             else []) ++-                                         (n, Just maxred) : specnames ++ +                                         (n, Just maxred) : specnames ++                                              concat descs)]                 logElab 3 $ "Specialising application: " ++ show specapp-                              ++ " in " ++ show caller ++-                              " with " ++ show opts+                              ++ "\n in \n" ++ show caller +++                              "\n with \n" ++ show opts+                              ++ "\nCalling: " ++ show cgns                 logElab 3 $ "New name: " ++ show newnm                 logElab 3 $ "PE definition type : " ++ (show specTy)                             ++ "\n" ++ show opts-                logElab 5 $ "PE definition " ++ show newnm ++ ":\n" +++                logElab 2 $ "PE definition " ++ show newnm ++ ":\n" ++                              showSep "\n"                                 (map (\ (lhs, rhs) ->                                   (showTmImpls lhs ++ " = " ++                                    showTmImpls rhs)) (pe_clauses specdecl)) -                logElab 2 $ show n ++ " transformation rule: " +++                logElab 5 $ show n ++ " transformation rule: " ++                            showTmImpls rhs ++ " ==> " ++ showTmImpls lhs                  elabType info defaultSyntax emptyDocstring [] fc opts newnm NoFC specTy@@ -434,16 +485,18 @@           -- if it doesn't work, just don't specialise. Could happen for lots           -- of valid reasons (e.g. local variables in scope which can't be           -- lifted out).-          (\e -> do logElab 3 $ "Couldn't specialise: " ++ (pshow ist e)+          (\e -> do logElab 5 $ "Couldn't specialise: " ++ (pshow ist e)                     return [])      hiddenToPH (PHidden _) = Placeholder     hiddenToPH x = x -    specName simpl (ImplicitS, tm)+    specName simpl (ImplicitS _, tm)         | (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))     specName simpl (ExplicitS, tm)         | (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))+    specName simpl (ConstraintS, tm) +        | (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))     specName simpl _ = Nothing      -- get the descendants of the name 'n' which are marked %static@@ -454,7 +507,7 @@                           i <- getIState                           let statics = filter (staticFn i) ns                           return (map (\n -> (n, Nothing)) statics)-        +     staticFn :: IState -> Name -> Bool     staticFn i n =  case lookupCtxt n (idris_flags i) of                             [opts] -> elem StaticFn opts@@ -464,7 +517,7 @@                            Just s -> not (or s)                            _ -> True -    concreteArg ist (ImplicitS, tm) = concreteTm ist tm+    concreteArg ist (ImplicitS _, tm) = concreteTm ist tm     concreteArg ist (ExplicitS, tm) = concreteTm ist tm     concreteArg ist _ = True @@ -484,18 +537,18 @@               [ty] -> let (specty_in, args') = specType args (explicitNames ty)                           specty = normalise (tt_ctxt ist) [] (finalise specty_in)                           t = mkPE_TyDecl ist args' (explicitNames specty) in-                          (t, (n, args'))+                          return (t, (n, args')) --                             (normalise (tt_ctxt ist) [] (specType args ty))-              _ -> error "Can't happen (getSpecTy)"+              _ -> ifail $ "Ambiguous name " ++ show n ++ " (getSpecTy)"      -- get the clause of a specialised application-    getSpecClause ist (n, args)+    getSpecClause ist (n, args) specTy        = let newnm = sUN ("PE_" ++ show (nsroot n) ++ "_" ++                                qhash 5381 (showSep "_" (map showArg args))) in                                -- UN (show n ++ show (map snd args)) in-             (n, newnm, mkPE_TermDecl ist newnm n args)+             (n, newnm, mkPE_TermDecl ist newnm n specTy args)       where showArg (ExplicitS, n) = qshow n-            showArg (ImplicitS, n) = qshow n+            showArg (ImplicitS _, n) = qshow n             showArg _ = ""              qshow (Bind _ _ _) = "fn"@@ -511,14 +564,18 @@             qhash hash (x:xs) = qhash (hash * 33 + fromIntegral(fromEnum x)) xs  -- | Checks if the clause is a possible left hand side.-checkPossible :: ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris Bool+-- NOTE: A lot of this is repeated for reflected definitions in Idris.Elab.Term+-- One day, these should be merged, but until then remember that if you edit+-- this you might need to edit the other version...+checkPossible :: ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris (Maybe PTerm) checkPossible info fc tcgen fname lhs_in    = do ctxt <- getContext         i <- getIState         let lhs = addImplPat i lhs_in+        logElab 10 $ "Trying missing case: " ++ showTmImpls lhs         -- if the LHS type checks, it is possible         case elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState-                            (erun fc (buildTC i info ELHS [] fname+                            (erun fc (buildTC i info EImpossible [] fname                                                 (allNamesIn lhs_in)                                                 (infTerm lhs))) of             OK (ElabResult lhs' _ _ ctxt' newDecls highlights newGName, _) ->@@ -526,15 +583,63 @@                   processTacticDecls info newDecls                   sendHighlighting highlights                   updateIState $ \i -> i { idris_name = newGName }-                  let lhs_tm = orderPats (getInferTerm lhs')-                  case recheck (constraintNS info) ctxt' [] (forget lhs_tm) lhs_tm of-                       OK _ -> return True-                       err -> return False+                  let lhs_tm = normalise ctxt [] (orderPats (getInferTerm lhs'))+                  let emptyPat = hasEmptyPat ctxt (idris_datatypes i) lhs_tm+                  if emptyPat then +                     do logElab 10 $ "Empty type in pattern "+                        return Nothing+                    else+                      case recheck (constraintNS info) ctxt' [] (forget lhs_tm) lhs_tm of+                           OK (tm, _, _) -> +                                    do logElab 10 $ "Valid " ++ show tm ++ "\n"+                                                 ++ " from " ++ show lhs+                                       return (Just (delab' i tm True True))+                           err -> do logElab 10 $ "Conversion failure"+                                     return Nothing             -- if it's a recoverable error, the case may become possible-            Error err -> if tcgen then return (recoverableCoverage ctxt err)-                                  else return (validCoverageCase ctxt err ||+            Error err -> do logLvl 10 $ "Impossible case " ++ (pshow i err)+                            -- tcgen means that it was generated by genClauses,+                            -- so only looking for an error. Otherwise, it+                            -- needs to be the right kind of error (a type mismatch+                            -- in the same family).+                            if tcgen then returnTm i err (recoverableCoverage ctxt err)+                                  else returnTm i err (validCoverageCase ctxt err ||                                                  recoverableCoverage ctxt err)+  where returnTm i err True = do logLvl 10 $ "Possibly resolvable error on " ++ +                                    pshow i (fmap (normalise (tt_ctxt i) []) err)+                                              ++ " on " ++ showTmImpls lhs_in+                                 return $ Just lhs_in+        returnTm i err False = return $ Nothing +-- Filter out the terms which are not well type left hand sides. Whenever we+-- eliminate one, also eliminate later ones which match it without checking,+-- because they're obviously going to have the same result+checkPossibles :: ElabInfo -> FC -> Bool -> Name -> [PTerm] -> Idris [PTerm]+checkPossibles info fc tcgen fname (lhs : rest)+   = do ok <- checkPossible info fc tcgen fname lhs+        i <- getIState+        -- Hypothesis: any we can remove will be within the next few, because+        -- leftmost patterns tend to change less+        -- Since the match could take a while if there's a lot of cases to+        -- check, just remove from the next batch+        let rest' = filter (\x -> not (qmatch x lhs)) (take 200 rest) ++ drop 200 rest+        restpos <- checkPossibles info fc tcgen fname rest'+        case ok of +             Nothing -> return restpos +             Just lhstm -> return (lhstm : restpos)+  where+    qmatch _ Placeholder = True+    qmatch (PApp _ f args) (PApp _ f' args')+       | length args == length args'+            = qmatch f f' && and (zipWith qmatch (map getTm args)+                                                 (map getTm args'))+    qmatch (PRef _ _ n) (PRef _ _ n') = n == n'+    qmatch (PPair _ _ _ l r) (PPair _ _ _ l' r') = qmatch l l' && qmatch r r' +    qmatch (PDPair _ _ _ l t r) (PDPair _ _ _ l' t' r') +          = qmatch l l' && qmatch t t' && qmatch r r' +    qmatch x y = x == y+checkPossibles _ _ _ _ [] = return []+ findUnique :: Context -> Env -> Term -> [Name] findUnique ctxt env (Bind n b sc)    = let rawTy = forgetEnv (map fst env) (binderTy b)@@ -547,6 +652,34 @@                  else findUnique ctxt ((n, b) : env) sc findUnique _ _ _ = [] +getUnfolds (UnfoldIface n ns : _) = Just (n, ns)+getUnfolds (_ : xs) = getUnfolds xs+getUnfolds [] = Nothing++-- Unfold the given name, interface methdods, and any function which uses it as+-- an argument directly. This is specifically for finding applications of+-- interface dictionaries and inlining them both for totality checking and for+-- a small performance gain.+getNamesToUnfold :: Name -> [Name] -> Term -> [Name]+getNamesToUnfold iname ms tm = nub $ iname : getNames Nothing tm ++ ms+  where+    getNames under fn@(App _ _ _)+        | (f, args) <- unApply fn+             = let under' = case f of+                                 P _ fn _ -> Just fn+                                 _ -> Nothing +                              in+                   getNames under f ++ concatMap (getNames under') args+    getNames (Just under) (P _ ref _)+        = if ref == iname then [under] else []+    getNames under (Bind n (Let t v) sc) +        = getNames Nothing t +++          getNames Nothing v +++          getNames Nothing sc+    getNames under (Bind n b sc) = getNames Nothing (binderTy b) +++                                   getNames Nothing sc+    getNames _ _ = []+ -- | Return the elaborated LHS/RHS, and the original LHS with implicits added elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->               Idris (Either Term (Term, Term), PTerm)@@ -556,12 +689,12 @@         let lhs = addImpl [] i lhs_in         b <- checkPossible info fc tcgen fname lhs_in         case b of-            True -> tclift $ tfail (At fc-                                (Msg $ show lhs_in ++ " is a valid case"))-            False -> do ptm <- mkPatTm lhs_in-                        logElab 5 $ "Elaborated impossible case " ++ showTmImpls lhs ++-                                    "\n" ++ show ptm-                        return (Left ptm, lhs)+            Just _ -> tclift $ tfail (At fc+                                 (Msg $ show lhs_in ++ " is a valid case"))+            Nothing -> do ptm <- mkPatTm lhs_in+                          logElab 5 $ "Elaborated impossible case " ++ showTmImpls lhs +++                                      "\n" ++ show ptm+                          return (Left ptm, lhs) elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as whereblock)    = do let tcgen = Dictionary `elem` opts         push_estack fname False@@ -630,7 +763,7 @@                                then recheckC_borrowing False (PEGenerated `notElem` opts)                                                        [] (constraintNS info) fc id [] lhs_tm                                else return (lhs_tm, lhs_ty)-        let clhs = Idris.Core.Evaluate.simplify ctxt [] clhs_c+        let clhs = normalise ctxt [] clhs_c         let borrowed = borrowedNames [] clhs          -- These are the names we're not allowed to use on the RHS, because@@ -685,7 +818,7 @@         logElab 2 $ "RHS: " ++ show (map fst newargs_all) ++ " " ++ showTmImpls rhs         ctxt <- getContext -- new context with where block added         logElab 5 "STARTING CHECK"-        ((rhs', defer, holes, is, probs, ctxt', newDecls, highlights, newGName), _) <-+        ((rhsElab, defer, holes, is, probs, ctxt', newDecls, highlights, newGName), _) <-            tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patRHS") clhsty initEState                     (do pbinds ist lhs_tm                         -- proof search can use explicitly written names@@ -714,7 +847,19 @@         when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)          logElab 5 "DONE CHECK"-        logElab 4 $ "---> " ++ show rhs'+        logElab 3 $ "---> " ++ show rhsElab+        ctxt <- getContext+        +        let rhs' = case getUnfolds opts of+                        Just (n, ms) -> +                           let ns = getNamesToUnfold n ms rhsElab in+                               unfold ctxt [] (map (\n -> (n, 1)) ns) rhsElab+                        _ -> rhsElab+        +        logElab 5 $ "----- " ++ show (getUnfolds opts) +++                    "\nUnfolded " ++ show rhsElab ++ "\n" +++                    "to " ++ show rhs'+         when (not (null defer)) $ logElab 1 $ "DEFERRED " ++                     show (map (\ (n, (_,_,t,_)) -> (n, t)) defer) @@ -767,14 +912,17 @@             Error e -> ierror (At fc (CantUnify False (clhsty, Nothing) (crhsty, Nothing) e [] 0))         i <- getIState         checkInferred fc (delab' i crhs True True) rhs-        -- if the function is declared '%error_reverse', or its type,+        -- if the function is declared '%error_reverse',         -- then we'll try running it in reverse to improve error messages+        -- Also if the type is '%error_reverse' and the LHS is smaller than+        -- the RHS         let (ret_fam, _) = unApply (getRetTy crhsty)         rev <- case ret_fam of                     P _ rfamn _ ->                         case lookupCtxt rfamn (idris_datatypes i) of                              [TI _ _ dopts _ _] ->-                                 return (DataErrRev `elem` dopts)+                                 return (DataErrRev `elem` dopts &&+                                         size clhs <= size crhs)                              _ -> return False                     _ -> return False @@ -872,13 +1020,15 @@         let ret_ty = getRetTy (explicitNames (normalise ctxt [] lhs_ty))         let static_names = getStaticNames i lhs_tm         logElab 5 (show lhs_tm ++ "\n" ++ show static_names)-        (clhs, clhsty) <- recheckC (constraintNS info) fc id [] lhs_tm+        (clhs_c, clhsty) <- recheckC (constraintNS info) fc id [] lhs_tm+        let clhs = normalise ctxt [] clhs_c+         logElab 5 ("Checked " ++ show clhs)         let bargs = getPBtys (explicitNames (normalise ctxt [] lhs_tm))         let wval = rhs_trans info $ addImplBound i (map fst bargs) wval_in         logElab 5 ("Checking " ++ showTmImpls wval)         -- Elaborate wval in this context-        ((wval', defer, is, ctxt', newDecls, highlights, newGName), _) <-+        ((wvalElab, defer, is, ctxt', newDecls, highlights, newGName), _) <-             tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "withRHS")                         (bindTyArgs PVTy bargs infP) initEState                         (do pbinds i lhs_tm@@ -900,8 +1050,19 @@         let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'         addDeferred def''         mapM_ (elabCaseBlock info opts) is++        let wval' = case getUnfolds opts of+                        Just (n, ms) -> +                           let ns = getNamesToUnfold n ms wvalElab in+                             unfold ctxt [] (map (\n -> (n, 1)) ns) wvalElab+                        _ -> wvalElab+                 logElab 5 ("Checked wval " ++ show wval')+        logElab 5 $ "----- " ++ show (getUnfolds opts) +++                    "\nUnfolded wval " ++ show wvalElab ++ "\n" +++                    "to " ++ show wval' +         ctxt <- getContext         (cwval, cwvalty) <- recheckC (constraintNS info) fc id [] (getInferTerm wval')         let cwvaltyN = explicitNames (normalise ctxt [] cwvalty)@@ -971,9 +1132,13 @@         wb <- mapM (mkAuxC mpn wname lhs (map fst bargs_pre) (map fst bargs_post))                        withblock         logElab 3 ("with block " ++ show wb)-        -- propagate totality assertion to the new definitions-        setFlags wname [Inlinable]-        when (AssertTotal `elem` opts) $ setFlags wname [Inlinable, AssertTotal]+        -- propagate totality assertion and unfold flags to the new definitions+        let uflags = case getUnfolds opts of+                          Just (n, ns) -> [UnfoldIface n ns]+                          _ -> []+        setFlags wname ([Inlinable] ++ uflags)+        when (AssertTotal `elem` opts) $ +           setFlags wname ([Inlinable, AssertTotal] ++ uflags)         i <- getIState         let rhstrans' = updateWithTerm i mpn wname lhs (map fst bargs_pre) (map fst (bargs_post))                              . rhs_trans info@@ -993,7 +1158,7 @@         logElab 5 ("New RHS " ++ showTmImpls rhs)         ctxt <- getContext -- New context with block added         i <- getIState-        ((rhs', defer, is, ctxt', newDecls, highlights, newGName), _) <-+        ((rhsElab, defer, is, ctxt', newDecls, highlights, newGName), _) <-            tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "wpatRHS") clhsty initEState                     (do pbinds i lhs_tm                         setNextName@@ -1003,9 +1168,22 @@                         tt <- get_term                         return (tt, d, is, ctxt', newDecls, highlights, newGName))         setContext ctxt'+                 processTacticDecls info newDecls         sendHighlighting highlights         updateIState $ \i -> i { idris_name = newGName }+        +        ctxt <- getContext+        let rhs' = case getUnfolds opts of+                        Just (n, ms) -> +                           let ns = getNamesToUnfold n ms rhsElab in+                             unfold ctxt [] (map (\n -> (n, 1)) ns) rhsElab+                        _ -> rhsElab+        +        logElab 5 $ "----- " ++ show (getUnfolds opts) +++                    "\nUnfolded with RHS " ++ show rhsElab ++ "\n" +++                    "to " ++ show rhs'+          def' <- checkDef info fc iderr True defer         let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'