idris 1.3.0 → 1.3.1

raw patch · 88 files changed

+1411/−378 lines, 88 filesdep ~aesondep ~megaparsecdep ~networkPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: aeson, megaparsec, network

API changes (from Hackage documentation)

Files

• .travis.yml +8/−6
• CHANGELOG.md +7/−0
• INSTALL.md +4/−1
• azure-pipelines.yml +143/−0
• docs/conf.py +1/−1
• docs/faq/faq.rst +28/−4
• docs/guides/type-providers-ffi.rst +1/−1
• 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/codegen.rst +5/−0
• docs/reference/elaborator-reflection.rst +2/−1
• docs/reference/ffi.rst +6/−0
• docs/tutorial/views.rst +11/−0
• idris-tutorial.pdf binary
• idris.cabal +4/−4
• libs/base/Control/Isomorphism.idr +12/−6
• libs/base/Data/Buffer.idr +5/−4
• libs/base/Data/Complex.idr +7/−12
• libs/base/Data/Morphisms.idr +43/−27
• libs/base/Data/Nat/Views.idr +1/−1
• libs/base/Data/Vect.idr +117/−19
• libs/contrib/Control/Algebra.idr +14/−0
• libs/contrib/Control/Isomorphism/Extra.idr +42/−0
• libs/contrib/Control/Isomorphism/Fin.idr +54/−0
• libs/contrib/Control/Isomorphism/Vect.idr +155/−0
• libs/contrib/Data/Fin/Extra.idr +2/−2
• libs/contrib/Data/Nat.idr +8/−0
• libs/contrib/Interfaces/Verified.idr +185/−29
• libs/contrib/Text/Lexer.idr +25/−1
• libs/contrib/Text/Lexer/Core.idr +1/−1
• libs/contrib/Text/Parser.idr +1/−1
• libs/contrib/Text/PrettyPrint/WL/Core.idr +2/−2
• libs/contrib/contrib.ipkg +6/−0
• libs/prelude/Builtins.idr +1/−0
• libs/prelude/Decidable/Equality.idr +16/−8
• libs/prelude/Prelude/Algebra.idr +0/−2
• libs/prelude/Prelude/Either.idr +4/−0
• libs/prelude/Prelude/File.idr +6/−0
• libs/prelude/Prelude/List.idr +44/−6
• libs/prelude/Prelude/Strings.idr +8/−0
• libs/prelude/Prelude/WellFounded.idr +5/−0
• man/idris.1 +1/−1
• rts/Makefile +7/−11
• rts/idris_buffer.c +7/−3
• rts/idris_buffer.h +1/−1
• rts/idris_main.c +1/−1
• rts/idris_rts.c +19/−4
• rts/idris_rts.h +10/−5
• rts/idris_stdfgn.c +8/−0
• rts/idris_stdfgn.h +2/−0
• src/IRTS/CodegenC.hs +83/−73
• src/IRTS/JavaScript/PrimOp.hs +4/−4
• src/IRTS/Lang.hs +25/−0
• src/IRTS/LangOpts.hs +56/−27
• src/IRTS/System.hs +1/−1
• src/Idris/AbsSyntaxTree.hs +6/−6
• src/Idris/Core/CaseTree.hs +4/−4
• src/Idris/Core/TT.hs +3/−3
• src/Idris/Directives.hs +7/−5
• src/Idris/Elab/Clause.hs +3/−5
• src/Idris/Elab/Data.hs +4/−3
• src/Idris/Elab/Interface.hs +6/−5
• src/Idris/Elab/Record.hs +5/−4
• src/Idris/Elab/Term.hs +5/−5
• src/Idris/Elab/Type.hs +2/−2
• src/Idris/Elab/Value.hs +1/−0
• src/Idris/ElabDecls.hs +3/−1
• src/Idris/Erasure.hs +3/−0
• src/Idris/IdrisDoc.hs +7/−8
• src/Idris/Main.hs +1/−2
• src/Idris/Output.hs +14/−12
• src/Idris/Parser.hs +6/−5
• src/Idris/Parser/Helpers.hs +2/−1
• src/Idris/Parser/Ops.hs +10/−1
• src/Idris/Parser/Stack.hs +2/−2
• src/Idris/Primitives.hs +5/−1
• src/Idris/REPL.hs +11/−7
• src/Util/Net.hs +9/−12
• stack-shell.nix +4/−2
• stack.yaml +1/−1
• test/disambig002/disambig002.idr +0/−5
• test/pkg008/expected +1/−1
• test/regression001/reg007.idr +69/−0
• test/regression001/run +1/−1
• test/regression002/Negation.idr +2/−0
• test/regression002/expected +1/−1
• test/regression002/run +1/−0

@@ -11,12 +11,13 @@   include:     - env: CABALVER="2.2" GHCVER="8.4.1" STACKVER="7.14" STYLISH=YES       addons: {apt: {packages: [cabal-install-2.2,ghc-8.4.1,hscolour], sources: [hvr-ghc]}}-    - env: CABALVER="1.22" GHCVER="7.10.3" TESTS="test_c"+    - env: CABALVER="2.2" GHCVER="7.10.3" TESTS="test_c"       compiler: ": #GHC 7.10.3"-      addons: {apt: {packages: [cabal-install-1.22,ghc-7.10.3,cppcheck,hscolour], sources: [hvr-ghc]}}-    - env: CABALVER="1.24" GHCVER="8.0.1" TESTS="test_c"-      compiler: ": #GHC 8.0.1"-      addons: {apt: {packages: [cabal-install-1.24,ghc-8.0.1,cppcheck,hscolour], sources: [hvr-ghc]}}+      addons: {apt: {packages: [cabal-install-2.2,ghc-7.10.3,cppcheck,hscolour], sources: [hvr-ghc]}}+# Disabled because it's always timing out+#    - env: CABALVER="1.24" GHCVER="8.0.1" TESTS="test_c"+#      compiler: ": #GHC 8.0.1"+#      addons: {apt: {packages: [cabal-install-1.24,ghc-8.0.1,cppcheck,hscolour], sources: [hvr-ghc]}}     - env: CABALVER="2.0" GHCVER="8.2.2" TESTS="lib_doc doc"       compiler: ": #GHC 8.2.2"       addons: {apt: {packages: [cabal-install-2.0,ghc-8.2.2,cppcheck,hscolour], sources: [hvr-ghc]}}@@ -26,7 +27,8 @@     - env: CABALVER="2.0" GHCVER="8.2.2" TESTS="test_c"       compiler: ": #GHC 8.2.2"       addons: {apt: {packages: [cabal-install-2.0,ghc-8.2.2,cppcheck,hscolour], sources: [hvr-ghc]}}-#TODO: Uncomment when tasty-rerun has been updated for base-4.11+#TODO: The idris built with those fails due to libffi dynamic linking version mismatch.+#      Caused by the GHC backport to Trusty? #    - env: CABALVER="2.2" GHCVER="8.4.1" TESTS="lib_doc doc" #      compiler: ": #GHC 8.4.1" #      addons: {apt: {packages: [cabal-install-2.2,ghc-8.4.1,cppcheck,hscolour], sources: [hvr-ghc]}}

@@ -1,3 +1,10 @@+# New in 1.3.1++## Tool updates++ Fixes for building with GHC 8.6++ Fix for megaparsec update++ Some fixes for memory allocation issues in the C back end+ # New in 1.3.0  ## Language updates

@@ -81,7 +81,10 @@ * `stack install`  Stack will install Idris (and related executables) into `$HOME/.local/bin/`-on Unix based systems and an appropriate place on Windows.+on Unix based systems and an appropriate place on Windows. The libraries that +are included with Idris (e.g. Builtins, Prelude) will 'install' into `<source +dir>/.stack_work/install/...` so you'll need to keep your source directory +around after you've installed Idris using Stack.  Of note: If you haven't used stack before commands will also setup the related infrastructure. For more information about Stack please visit

@@ -0,0 +1,143 @@+# Starter pipeline+# Start with a minimal pipeline that you can customize to build and deploy your code.+# Add steps that build, run tests, deploy, and more:+# https://aka.ms/yaml+jobs:+  # Test a configuration with the oldest supported GHC+  - job: Linux_GHC_710+    pool:+      vmImage: 'Ubuntu 16.04'+    steps:+    - script: |+        sudo add-apt-repository ppa:hvr/ghc+        sudo apt-get update+        sudo apt-get install ghc-7.10.3 cabal-install-2.2+        sudo update-alternatives --config opt-ghc+        sudo update-alternatives --config opt-cabal+      displayName: 'Prepare system'+    - script: |+        export PATH=/opt/ghc/bin:$HOME/.cabal/bin:$PATH+        cabal update+        CABALFLAGS="-fffi -fci" make+      displayName: 'Build Idris'+    - script: |+        export PATH=/opt/ghc/bin:$HOME/.cabal/bin:$PATH+        make test_c+      displayName: 'Run tests'+  # Test on Linux+  - job: Linux+    pool:+      vmImage: 'Ubuntu 16.04'+    steps:+    - script: |+        sudo add-apt-repository ppa:hvr/ghc+        sudo apt-get update+        sudo apt-get install ghc-8.2.2 cabal-install-2.2+        sudo update-alternatives --config opt-ghc+        sudo update-alternatives --config opt-cabal+      displayName: 'Prepare system'+    - script: |+        export PATH=/opt/ghc/bin:$HOME/.cabal/bin:$PATH+        cabal update+        CABALFLAGS="-fffi -fci" make+      displayName: 'Build Idris'+    - script: |+        export PATH=/opt/ghc/bin:$HOME/.cabal/bin:$PATH+        make test_c+      displayName: 'Run tests'+  # Test on MacOS +  - job: macOS+    pool:+      vmImage: 'xcode9-macos10.13'+    steps:+    - script: |+        brew install ghc cabal-install libffi pkgconfig+        export PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig:$PKG_CONFIG_PATH+        export PATH=$HOME/.cabal/bin:$PATH+        cabal update+        CABALFLAGS="-fffi -fci" make+        make test_c+      displayName: 'Build idris and run tests'+  # Test on Windows+  - job: Windows+    pool:+      vmImage: 'vs2017-win2016'+    steps:+    - powershell: |+        choco install cabal -y --no-progress+        choco install 7zip.portable -y --no-progress+        choco install msys2 -y --no-progress --params "/InstallDir=C:/msys64/"+        mkdir C:\ghc+        Invoke-WebRequest "http://downloads.haskell.org/~ghc/8.4.3/ghc-8.4.3-x86_64-unknown-mingw32.tar.xz" -OutFile C:\ghc\ghc.tar.xz -UserAgent "Curl"+        7z x C:\ghc\ghc.tar.xz -oC:\ghc+        7z x C:\ghc\ghc.tar -oC:\ghc+      displayName: "Setting up environment"+    - powershell: |+        cabal update+        $env:PATH="$env:PATH;$HOME\AppData\Roaming\cabal\bin;c:\ghc\ghc-8.4.3\bin"+        $env:current_posix=c:\msys64\usr\bin\cygpath -u $(pwd)+        c:\msys64\usr\bin\bash -l -c "echo `$MSYSTEM && echo `$PATH"+        c:\msys64\usr\bin\bash -l -c "pacman -S make mingw-w64-x86_64-gcc mingw-w64-x86_64-pkg-config mingw-w64-x86_64-libffi --noconfirm 2>&1"+        c:\msys64\usr\bin\bash -l -c "cd $env:current_posix && cabal install -fffi --enable-test 2>&1"+        c:\msys64\usr\bin\bash -l -c "cd $env:current_posix && make test_c 2>&1"+      env:+        MSYSTEM: MINGW64+        MSYS2_PATH_TYPE: inherit+      displayName: "Build and test Idris"+  # Check styling+  - job: Stylize+    pool:+      vmImage: 'Ubuntu 16.04'+    steps:+    - script: |+        sudo add-apt-repository ppa:hvr/ghc+        sudo apt-get update+        sudo apt-get install ghc-8.2.2 cabal-install-2.2+        sudo update-alternatives --config opt-ghc+        sudo update-alternatives --config opt-cabal+      displayName: 'Prepare system'+    - script: |+        export PATH=/opt/ghc/bin:$HOME/.cabal/bin:$PATH+        cabal update+        cabal install stylish-haskell+        ./stylize.sh+      displayName: 'Run stylish'+  # Run tests on the node backend+  - job: JS+    pool:+      vmImage: 'Ubuntu 16.04'+    steps:+    - script: |+        sudo add-apt-repository ppa:hvr/ghc+        sudo apt-get update+        sudo apt-get install ghc-8.2.2 cabal-install-2.2+        sudo update-alternatives --config opt-ghc+        sudo update-alternatives --config opt-cabal+      displayName: 'Prepare system'+    - script: |+        export PATH=/opt/ghc/bin:$HOME/.cabal/bin:$PATH+        cabal update+        CABALFLAGS="-fffi -fci" make+      displayName: 'Build Idris'+    - script: |+        export PATH=/opt/ghc/bin:$HOME/.cabal/bin:$PATH+        make test_js+      displayName: 'Run tests'+  # Build docs+  - job: Docs+    pool:+      vmImage: 'Ubuntu 16.04'+    steps:+    - script: |+        sudo add-apt-repository ppa:hvr/ghc+        sudo apt-get update+        sudo apt-get install ghc-8.2.2 cabal-install-2.2+        sudo update-alternatives --config opt-ghc+        sudo update-alternatives --config opt-cabal+      displayName: 'Prepare system'+    - script: |+        export PATH=/opt/ghc/bin:$HOME/.cabal/bin:$PATH+        cabal update+        CABALFLAGS="-fffi -fci" make+        make lib_doc doc+      displayName: 'Build Docs'

@@ -61,7 +61,7 @@ # The short X.Y version. version = '1.3' # The full version, including alpha/beta/rc tags.-release = '1.3.0'+release = '1.3.1'  # The language for content autogenerated by Sphinx. Refer to documentation # for a list of supported languages.

@@ -33,7 +33,31 @@ limited to) extra library support, polishing the run-time system (and ensuring it is robust), providing and maintaining a JVM back end, etc. +Is there some documentation for the standard lib? List of functions?+===================================================================== +API documentation for the shipped packages is listed on `the+documentation page <http://www.idris-lang.org/documentation/>`_.++Unfortunately, the default prelude and shipped packages for `Idris`+are not necessarily complete with regards to documentation.  Other+ways to find functions include:+++ REPL commands:++  + Use `:apropos` to search for text in documentation and function names.+  + Use `:search` to search for functions of a given type.+  + Use `:browse` to list the contents of a given namespace.+++ Use the REPL's auto-complete functionality.++ Grep through the source code in `libs/`++If you find that the shipped packages are lacking in documentation,+please feel free to write some. Or bug someone to do so.  `Idris` has+syntax for providing rich documentation, which is then viewable using+the `:doc` command and listed in generated HTML API documentation.++ Why does Idris use eager evaluation rather than lazy? ===================================================== @@ -191,10 +215,10 @@ When will Idris be self-hosting? ================================ -It’s not a priority, though not a bad idea in the long run. It would be a-worthwhile effort in the short term to implement libraries to support-self-hosting, such as a good parsing library.-+It’s not a priority, though not a bad idea in the long run. It would+be a worthwhile effort in the short term to implement libraries in+Idris to support self-hosting, such as argument parsing and a+POSIX-compliant library for system interaction.  Does Idris have universe polymorphism? What is the type of ``Type``? ====================================================================

@@ -3,7 +3,7 @@ ***********************  `Type providers in Idris-<http://www.itu.dk/people/drc/pubs/dependent-type-providers.pdf>`__+<http://www.davidchristiansen.dk/pubs/dependent-type-providers.pdf>`__ are simple enough, but there are a few caveats to using them that it would be worthwhile to go through the basic steps. We also go over foreign functions, because these will often be used with type

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

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

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

@@ -131,3 +131,8 @@ ---  `Available online <https://github.com/edwinb/WS-idr>`__++WebAssembly+-----------++`Available online <https://github.com/SPY/idris-codegen-wasm>`__

@@ -6,7 +6,8 @@  The Idris elaborator is responsible for converting high-level Idris code into the core language. It is implemented as a kind of embedded tactic language in Haskell, where tactic scripts are written in an *elaboration monad* that provides error handling and a proof state.-For details, see [Edwin Brady's 2013 paper in the Journal of Functional Programming](https://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf).+For details, see `Edwin Brady's 2013 paper in the Journal of Functional+Programming <https://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf>`_.  Elaborator reflection makes the elaboration type as well as a selection of its tactics available to Idris code. This means that metaprograms written in Idris can have complete control over the elaboration process, generating arbitrary code, and they have access to all of the facilities available in the elaborator, such as higher-order unification, type checking, and emitting auxiliary definitions.

@@ -178,6 +178,12 @@     example : (Int -> ()) -> IO ()     example f = foreign FFI_C "callbacker" (CFnPtr (Int -> ()) -> IO ()) f +Note that the function that is used as a callback can't be a closure, that is+it can't be a partially applied function. This is because the mechanism used is+unable to pass the closed-over values through C. If we want to pass Idris values+to the callback we have to pass them through C explicitly. Non-primitive Idris+values can be passed to C via the ``Raw`` type.+ The other big limitation is that it doesn't support IO functions. Use ``unsafePerformIO`` to wrap them (i.e. to make an IO function usable as a callback, change the return type from IOr to r, and change the = do to = unsafePerformIO $ do).

@@ -58,6 +58,17 @@     filter p (x :: xs) with (filter p xs)       | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' ) +``with`` clauses can also be nested:++.. code-block:: idris++    foo : Int -> Int -> Bool+    foo n m with (succ n)+      foo _ m | 2 with (succ m)+        foo _ _ | 2 | 3 = True+        foo _ _ | 2 | _ = False+      foo _ _ | _ = False+ If the intermediate computation itself has a dependent type, then the result can affect the forms of other arguments — we can learn the form of one value by testing another. In these cases, view refined argument

binary file changed (658507 → 661109 bytes)

@@ -1,5 +1,5 @@ Name:           idris-Version:        1.3.0+Version:        1.3.1 License:        BSD3 License-file:   LICENSE Author:         Edwin Brady@@ -270,7 +270,7 @@                 , BuildFlags_idris    Build-depends:  base >=4 && <5-                , aeson >= 0.6 && < 1.3+                , aeson >= 0.6 && < 1.4                 , annotated-wl-pprint >= 0.7 && < 0.8                 , ansi-terminal < 0.9                 , ansi-wl-pprint < 0.7@@ -289,9 +289,9 @@                 , fingertree >= 0.1.4.1 && < 0.2                 , haskeline >= 0.7 && < 0.8                 , ieee754 >= 0.7 && < 0.9-                , megaparsec >= 6.2+                , megaparsec >= 6.2 && < 7                 , mtl >= 2.1 && < 2.3-                , network < 2.7+                , network < 2.8                 , optparse-applicative >= 0.13 && < 0.15                 , pretty < 1.2                 , process < 1.7

@@ -8,12 +8,12 @@ %access public export  ||| An isomorphism between two types-data Iso : Type -> Type -> Type where-  MkIso : (to : a -> b) ->-          (from : b -> a) ->-          (toFrom : (y : b) -> to (from y) = y) ->-          (fromTo : (x : a) -> from (to x) = x) ->-          Iso a b+record Iso a b where+  constructor MkIso+  to : a -> b+  from : b -> a+  toFrom : (y : b) -> to (from y) = y+  fromTo : (x : a) -> from (to x) = x  -- Isomorphism properties @@ -36,6 +36,12 @@ Category Iso where   id = isoRefl   (.) = flip isoTrans++Semigroup (Iso a a) where+  (<+>) = isoTrans++Monoid (Iso a a) where+  neutral = isoRefl  ||| Isomorphism is symmetric isoSym : Iso a b -> Iso b a

@@ -21,11 +21,12 @@ ||| fails export newBuffer : (size : Int) -> IO (Maybe Buffer)-newBuffer size = do bptr <- foreign FFI_C "idris_newBuffer" (Int -> IO Ptr) -                                    size-                    bad <- nullPtr bptr+newBuffer size = do vm <- getMyVM+                    bptr <- foreign FFI_C "idris_newBuffer" (Ptr -> Int -> IO ManagedPtr) +                                    vm size+                    bad <- nullManagedPtr bptr                     if bad then pure Nothing-                           else pure (Just (MkBuffer (prim__registerPtr bptr (size + 8)) size 0))+                           else pure (Just (MkBuffer bptr size 0))  ||| Reset the 'next location' pointer of the buffer to 0. ||| The 'next location' pointer gives the location for the next file read/write

@@ -27,19 +27,7 @@             plus_i = User 6  --- when we have an interface 'Fractional' (which contains Double),--- we can do:-{--implementation Fractional a => Fractional (Complex a) where-    (/) (a:+b) (c:+d) = let-                          real = (a*c+b*d)/(c*c+d*d)-                          imag = (b*c-a*d)/(c*c+d*d)-                        in-                          (real:+imag)--} -- ------------------------------ Polarform  mkPolar : Double -> Double -> Complex Double@@ -78,3 +66,10 @@ -- operates on Double. implementation Abs (Complex Double) where     abs (a:+b) = (magnitude (a:+b):+0)++implementation (Neg a, Fractional a) => Fractional (Complex a) where+    (/) (a:+b) (c:+d) = let+                          real = (a*c+b*d)/(c*c+d*d)+                          imag = (b*c-a*d)/(c*c+d*d)+                        in+                          (real:+imag)

@@ -1,54 +1,70 @@ module Data.Morphisms +%default total %access public export -data Morphism : Type -> Type -> Type where-  Mor : (a -> b) -> Morphism a b--data Endomorphism : Type -> Type where-  Endo : (a -> a) -> Endomorphism a--data Kleislimorphism : (Type -> Type) -> Type -> Type -> Type where-  Kleisli : Monad m => (a -> m b) -> Kleislimorphism m a b--applyKleisli : Monad m => (Kleislimorphism m a b) -> a -> m b-applyKleisli (Kleisli f) a = f a+record Morphism a b where+  constructor Mor+  applyMor : a -> b+infixr 1 ~>+(~>) : Type -> Type -> Type+(~>) = Morphism -applyMor : Morphism a b -> a -> b-applyMor (Mor f) a = f a+record Endomorphism a where+  constructor Endo+  applyEndo : a -> a -applyEndo : Endomorphism a -> a -> a-applyEndo (Endo f) a = f a+record Kleislimorphism (f : Type -> Type) a b where+  constructor Kleisli+  applyKleisli : a -> f b -implementation Functor (Morphism r) where-  map f (Mor a) = Mor (f . a)+Functor (Morphism r) where+  map f (Mor a) = Mor $ f . a -implementation Applicative (Morphism r) where-  pure a                = Mor $ const a+Applicative (Morphism r) where+  pure a = Mor $ const a   (Mor f) <*> (Mor a) = Mor $ \r => f r $ a r -implementation Monad (Morphism r) where+Monad (Morphism r) where   (Mor h) >>= f = Mor $ \r => applyMor (f $ h r) r -implementation Semigroup (Endomorphism a) where+Semigroup a => Semigroup (Morphism r a) where+  f <+> g = [| f <+> g |]++Monoid a => Monoid (Morphism r a) where+  neutral = [| neutral |]++Semigroup (Endomorphism a) where   (Endo f) <+> (Endo g) = Endo $ g . f -implementation Monoid (Endomorphism a) where+Monoid (Endomorphism a) where   neutral = Endo id -infixr 1 ~>+Functor f => Functor (Kleislimorphism f a) where+  map f (Kleisli g) = Kleisli (map f . g) -(~>) : Type -> Type -> Type-a ~> b = Morphism a b+Applicative f => Applicative (Kleislimorphism f a) where+  pure a = Kleisli $ const $ pure a+  (Kleisli f) <*> (Kleisli a) = Kleisli $ \r => f r <*> a r +Monad f => Monad (Kleislimorphism f a) where+  (Kleisli f) >>= g = Kleisli $ \r => applyKleisli (g !(f r)) r++-- Applicative is a bit too strong, but there is no suitable superclass+(Semigroup a, Applicative f) => Semigroup (Kleislimorphism f r a) where+  f <+> g = [| f <+> g |]++(Monoid a, Applicative f) => Monoid (Kleislimorphism f r a) where+  neutral = [| neutral |]+ Cast (Endomorphism a) (Morphism a a) where   cast (Endo f) = Mor f  Cast (Morphism a a) (Endomorphism a) where   cast (Mor f) = Endo f -Monad m => Cast (Morphism a (m b)) (Kleislimorphism m a b) where+Cast (Morphism a (f b)) (Kleislimorphism f a b) where   cast (Mor f) = Kleisli f -Cast (Kleislimorphism m a b) (Morphism a (m b)) where+Cast (Kleislimorphism f a b) (Morphism a (f b)) where   cast (Kleisli f) = Mor f

@@ -14,7 +14,7 @@      HalfRecOdd : {n : Nat} -> (rec : Lazy (HalfRec n)) -> HalfRec (S (n + n))  ||| Covering function for the `Half` view-export+public export half : (n : Nat) -> Half n half Z = HalfEven {n=0} half (S k) with (half k)

@@ -293,7 +293,6 @@        Just y  => (S len ** y :: ys)        Nothing => (  len **      ys) - -------------------------------------------------------------------------------- -- Folds --------------------------------------------------------------------------------@@ -321,6 +320,7 @@ ||| Foldl without seeding the accumulator foldl1 : (t -> t -> t) -> Vect (S n) t -> t foldl1 f (x::xs) = foldl f x xs+ -------------------------------------------------------------------------------- -- Scans --------------------------------------------------------------------------------@@ -455,13 +455,17 @@ -- Splitting and breaking lists -------------------------------------------------------------------------------- -||| A tuple where the first element is a Vect of the n first elements and-||| the second element is a Vect of the remaining elements of the original Vect-||| It is equivalent to (take n xs, drop n xs)+||| A tuple where the first element is a `Vect` of the `n` first elements and+||| the second element is a `Vect` of the remaining elements of the original.+||| It is equivalent to `(take n xs, drop n xs)` (`splitAtTakeDrop`),+||| but is more efficient.+||| ||| @ n   the index to split at-||| @ xs  the Vect to split in two+||| @ xs  the `Vect` to split in two splitAt : (n : Nat) -> (xs : Vect (n + m) elem) -> (Vect n elem, Vect m elem)-splitAt n xs = (take n xs, drop n xs)+splitAt Z xs = ([], xs)+splitAt (S k) (x :: xs) with (splitAt k xs)+  | (tk, dr) = (x :: tk, dr)  partition : (elem -> Bool) -> Vect len elem -> ((p ** Vect p elem), (q ** Vect q elem)) partition p []      = ((_ ** []), (_ ** []))@@ -521,12 +525,14 @@ range {len=Z}   = [] range {len=S _} = FZ :: map FS range -||| Transpose a Vect of Vects, turning rows into columns and vice versa.+||| Transpose a `Vect` of `Vect`s, turning rows into columns and vice versa. |||+||| This is like zipping all the inner `Vect`s together and is equivalent to `traverse id` (`transposeTraverse`).+||| ||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.-transpose : {n : Nat} -> Vect m (Vect n elem) -> Vect n (Vect m elem)-transpose []        = replicate _ []-transpose (x :: xs) = zipWith (::) x (transpose xs)+transpose : Vect m (Vect n elem) -> Vect n (Vect m elem)+transpose []        = replicate _ []                -- = [| [] |]+transpose (x :: xs) = zipWith (::) x (transpose xs) -- = [| x :: xs |]  -------------------------------------------------------------------------------- -- Applicative/Monad/Traversable@@ -534,7 +540,6 @@  implementation Applicative (Vect k) where     pure = replicate _-     fs <*> vs = zipWith apply fs vs  ||| This monad is different from the List monad, (>>=)@@ -543,8 +548,8 @@     m >>= f = diag (map f m)  implementation Traversable (Vect n) where-    traverse f [] = pure Vect.Nil-    traverse f (x::xs) = [| Vect.(::) (f x) (traverse f xs) |]+    traverse f []        = [| [] |]+    traverse f (x :: xs) = [| f x :: traverse f xs |]  -------------------------------------------------------------------------------- -- Show@@ -554,12 +559,28 @@     show = show . toList  --------------------------------------------------------------------------------+-- Uninhabited+--------------------------------------------------------------------------------++Uninhabited a => Uninhabited (Vect (S n) a) where+    uninhabited (x :: _) = uninhabited x++-------------------------------------------------------------------------------- -- Properties -------------------------------------------------------------------------------- +vectMustBeNil : (xs : Vect Z a) -> xs = []+vectMustBeNil [] = Refl+ vectConsCong : (x : elem) -> (xs : Vect len elem) -> (ys : Vect m elem) -> (xs = ys) -> (x :: xs = x :: ys) vectConsCong x xs xs Refl = Refl +vectInjective1 : {xs : Vect n a} -> {ys : Vect m b} -> x :: xs ~=~ y :: ys -> x ~=~ y+vectInjective1 Refl = Refl++vectInjective2 : {xs : Vect n a} -> {ys : Vect m b} -> x :: xs ~=~ y :: ys -> xs ~=~ ys+vectInjective2 Refl = Refl+ vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs vectNilRightNeutral [] = Refl vectNilRightNeutral (x :: xs) =@@ -573,15 +594,92 @@ vectAppendAssociative (x :: xs) ys zs =   vectConsCong _ _ _ (vectAppendAssociative xs ys zs) +||| Adding a prefix and then taking the prefix gets the prefix. Or,+||| adding a suffix and then dropping the suffix does nothing.+takePrefix : (ns : Vect n a) -> (ms : Vect m a) -> take n (ns ++ ms) = ns+takePrefix [] _ = Refl+takePrefix (n :: ns) ms = cong $ takePrefix ns ms++||| Adding a prefix and then dropping the prefix does nothing. Or,+||| adding a suffix and then taking the suffix gets the suffix.+dropPrefix : (ns : Vect n a) -> (ms : Vect m a) -> drop n (ns ++ ms) = ms+dropPrefix [] ms = Refl+dropPrefix (_ :: ns) ms = dropPrefix ns ms++||| `take n . take (n + m) = take n`+takeTake : (n : Nat) -> (m : Nat) ->+           (xs : Vect ((n + m) + l) a) -> (ys : Vect (n + (m + l)) a) ->+           xs ~=~ ys ->+           take n (take (n + m) xs) = take n ys+takeTake Z m _ _ _ = Refl+takeTake (S n) m (x :: xs) (y :: ys) prf = rewrite vectInjective1 prf in cong (takeTake n m xs ys (vectInjective2 prf))++||| `drop (n + m) = drop m . drop n`+dropDrop : (n : Nat) -> (m : Nat) ->+           (xs : Vect ((n + m) + l) a) -> (ys : Vect (n + (m + l)) a) ->+           xs ~=~ ys ->+           drop (n + m) xs = drop m (drop n ys)+dropDrop Z m xs xs Refl = Refl+dropDrop (S n) m (_ :: xs) (_ :: ys) prf = dropDrop n m xs ys (vectInjective2 prf)++||| A `Vect` may be restored from its components.+takeDropConcat : (n : Nat) -> (xs : Vect (n + m) a) -> take n xs ++ drop n xs = xs+takeDropConcat Z xs = Refl+takeDropConcat (S n) (x :: xs) = cong $ takeDropConcat n xs++||| `drop n . take (n + m) = take m . drop n`.+|||+||| Or: there are two ways to extract a subsequence.+dropTakeTakeDrop : (n : Nat) -> (m : Nat) ->+                   (xs : Vect ((n + m) + l) a) -> (ys : Vect (n + (m + l)) a) ->+                   xs ~=~ ys ->+                   drop n (take (n + m) xs) = take m (drop n ys)+dropTakeTakeDrop Z m xs xs Refl = Refl+dropTakeTakeDrop (S n) m (_ :: xs) (_ :: ys) prf = dropTakeTakeDrop n m xs ys (vectInjective2 prf)++splitAtTakeDrop : (n : Nat) -> (xs : Vect (n + m) a) -> splitAt n xs = (take n xs, drop n xs)+splitAtTakeDrop Z xs = Refl+splitAtTakeDrop (S k) (x :: xs) with (splitAt k xs) proof p+  | (tk, dr) = let prf = trans p (splitAtTakeDrop k xs)+                in aux (cong {f=(x ::) . fst} prf) (cong {f=snd} prf)+  where aux : {a, b : Type} -> {w, x : a} -> {y, z : b} -> w = x -> y = z -> (w, y) = (x, z)+        aux Refl Refl = Refl++zipWithIsLiftA2 : (f : a -> b -> c) -> (as : Vect n a) -> (bs : Vect n b) -> zipWith f as bs = [| f as bs |]+zipWithIsLiftA2 _ [] [] = Refl+zipWithIsLiftA2 f (a :: as) (b :: bs) = rewrite zipWithIsLiftA2 f as bs in Refl+zipWithIsLiftA3 : (f : a -> b -> c -> d) -> (as : Vect n a) -> (bs : Vect n b) -> (cs : Vect n c) -> zipWith3 f as bs cs = [| f as bs cs |]+zipWithIsLiftA3 _ [] [] [] = Refl+zipWithIsLiftA3 f (a :: as) (b :: bs) (c :: cs) = rewrite zipWithIsLiftA3 f as bs cs in Refl++-- Note relationship to Applicative (Morphism (Fin n))+indexReplicate : (x : a) -> (n : Nat) -> (i : Fin n) -> index i (replicate n x) = x+indexReplicate x (S n) FZ = Refl+indexReplicate x (S n) (FS i) = indexReplicate x n i+indexZipWith : (f : a -> b -> c) -> (as : Vect n a) -> (bs : Vect n b) -> (i : Fin n) -> index i (zipWith f as bs) = f (index i as) (index i bs)+indexZipWith f (a :: _) (b :: _) FZ = Refl+indexZipWith f (_ :: as) (_ :: bs) (FS i) = indexZipWith f as bs i+indexTranspose : (x : Fin o) -> (y : Fin i) -> (xss : Vect o (Vect i a)) -> index y (index x xss) = index x (index y (transpose xss))+indexTranspose x y (xs :: xss) = rewrite prf in+                                 rewrite sym $ indexZipWith Vect.(::) xs (transpose xss) y in Refl+  where prf : index y (index x (xs :: xss)) = index x (index y xs :: index y (transpose xss))+        prf = case x of+                   FZ => Refl+                   FS k => indexTranspose k y xss++transposeTraverse : (xss : Vect o (Vect i a)) -> transpose xss = traverse Basics.id xss+transposeTraverse [] = Refl+transposeTraverse (xs :: xss) = rewrite zipWithIsLiftA2 Vect.(::) xs (transpose xss) in cong (transposeTraverse xss)++traverseIdCons : (xs : Vect o a) -> (xss : Vect o (Vect i a)) -> traverse Basics.id [| xs :: xss |] = xs :: traverse Basics.id xss+traverseIdCons [] [] = Refl+traverseIdCons (x :: xs) (ys :: xss) = rewrite traverseIdCons xs xss in Refl+transposeCons : (xs : Vect o a) -> (xss : Vect o (Vect i a)) -> transpose (zipWith (::) xs xss) = xs :: transpose xss+transposeCons xs xss = rewrite zipWithIsLiftA2 Vect.(::) xs xss in rewrite transposeTraverse (pure (::) <*> xs <*> xss) in rewrite transposeTraverse xss in traverseIdCons xs xss+ -------------------------------------------------------------------------------- -- DecEq ----------------------------------------------------------------------------------vectInjective1 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> x = y-vectInjective1 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl--vectInjective2 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> xs = ys-vectInjective2 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl  implementation DecEq a => DecEq (Vect n a) where   decEq [] [] = Yes Refl

@@ -126,6 +126,20 @@ pow' _ Z     = unity pow' x (S n) = x <.> pow' x n +-- TODO: This can be more efficient:+-- stimes 5 x = x <+> (x <+> (x <+> (x <+> x)))+--            = x <+> ((x <+> x) <+> (x <+> x))+--            = let y = x <+> x in x <+> (y <+> y)+-- 4 <+>s into 3 <+>+||| Combine `n` copies of a value with `<+>`+stimes : Semigroup a => (n : Nat) -> {auto prf : IsSucc n} -> a -> a+stimes (S Z) x = x+stimes (S (S k)) x = x <+> stimes (S k) x++||| Like `stimes`, but accepting `Z` as argument.+mtimes : Monoid a => (n : Nat) -> a -> a+mtimes Z x = neutral+mtimes (S k) x = stimes (S k) x  -- XXX todo: --   Structures where "abs" make sense.

@@ -0,0 +1,42 @@+module Control.Isomorphism.Extra++import Control.Isomorphism+import Interfaces.Verified++%default total+%access public export++||| Form an `Iso` that is the identity for almost all inputs, except it will swap either of the arguments for the other.+||| It is the same function in both directions.+|||+||| @ l the value that will be turned into `r`+||| @ r the value that will be turned into `l`+swapped : DecEq a => (l : a) -> (r : a) -> Iso a a+swapped {a} l r = MkIso swap swap prf prf+  where swap : a -> a+        swap x = case decEq l x of { Yes _ => r; No _ => case decEq r x of { Yes _ => l; No _ => x } }+        prf : (x : a) -> swap (swap x) = x+        prf x with (decEq l x)+          | (Yes lex) with (decEq r x)+            | (Yes rex) with (decEq l r)+              | (Yes ler) = rex+              | (No lnr) = absurd $ lnr $ trans lex $ sym rex+            | (No rnx) with (decEq l r)+              | (Yes ler) = absurd $ rnx $ trans (sym ler) lex+              | (No lnr) with (decEq r r)+                | (Yes Refl) = lex+                | (No rnr) = absurd $ rnr Refl+          | (No lnx) with (decEq r x)+            | (Yes rex) with (decEq l l)+              | (Yes Refl) = rex+              | (No lnl) = absurd $ lnl Refl+            | (No rnx) with (decEq l x)+              | (Yes lex) = absurd $ lnx lex+              | (No lnx') with (decEq r x)+                | (Yes rex) = absurd $ rnx rex+                | (No rnx') = Refl++mapIso : VerifiedFunctor f => Iso a b -> Iso (f a) (f b)+mapIso {f} (MkIso to from toFrom fromTo) = MkIso (map to) (map from) (prf to from toFrom) (prf from to fromTo)+  where prf : {a : Type} -> {b : Type} -> (to : a -> b) -> (from : b -> a) -> (toFrom : (x : b) -> to (from x) = x) -> (x : f b) -> map to (map from x) = x+        prf to' from' toFrom' x = rewrite sym $ functorComposition x from' to' in functorIdentity (to' . from') toFrom' x

@@ -0,0 +1,54 @@+module Control.Isomorphism.Fin++import Control.Isomorphism+import Data.Fin++%default total+%access public export++strengthenLeft : (i : Fin (S n)) -> (prf : strengthen i = Left x) -> i = Fin.last+strengthenLeft {n = Z} FZ Refl = Refl+strengthenLeft {n = S _} FZ Refl impossible+strengthenLeft {n = S k} (FS x) prf with (strengthen x) proof p+  | (Left l) = rewrite strengthenLeft x (sym p) in Refl+  | (Right r) = absurd $ leftNotRight $ sym prf+strengthenRight : (i : Fin (S n)) -> (prf : strengthen i = Right x) -> weaken x = i+strengthenRight {n = Z} FZ Refl impossible+strengthenRight {n = S _} FZ Refl = Refl+strengthenRight {n = S k} (FS x) prf with (strengthen x) proof p+  | (Left l) = absurd $ leftNotRight prf+  | (Right r) = rewrite rightInjective $ sym prf in rewrite strengthenRight x $ sym p in Refl+strengthenLast : (n : Nat) -> strengthen (last {n=n}) = Left last+strengthenLast Z = Refl+strengthenLast (S k) with (strengthen (last {n=k})) proof p+  | (Left l) = cong {f = Left . FS} $ leftInjective $ trans p $ strengthenLast k+  | (Right _) with (trans p (strengthenLast k))+    | Refl impossible+strengthenWeaken : (n : Fin k) -> strengthen (weaken n) = Right n+strengthenWeaken FZ = Refl+strengthenWeaken (FS n) with (strengthen (weaken n)) proof p+  | (Left _) with (trans p (strengthenWeaken n))+    | Refl impossible+  | (Right r) = cong {f = Right . FS} $ rightInjective $ trans p $ strengthenWeaken n++||| Sends `FZ` to `last`, and `FS x` to `x`.+rotatedDown : Iso (Fin n) (Fin n)+rotatedDown = MkIso to from toFrom fromTo+  where to : Fin k -> Fin k+        to FZ = last+        to (FS x) = weaken x+        from : Fin k -> Fin k+        from {k = Z} _ impossible+        from {k = S k} j = either (const FZ) FS $ strengthen j+        toFrom : (j : Fin k) -> to (from j) = j+        toFrom {k = S Z} FZ = Refl+        toFrom {k = S (S k)} FZ = Refl+        toFrom {k = S (S k)} (FS i) with (strengthen i) proof p+          toFrom {k = S (S k)} (FS i) | (Left l) = rewrite strengthenLeft i (sym p) in Refl+          toFrom {k = S (S k)} (FS i) | (Right r) = rewrite strengthenRight i (sym p) in Refl+        fromTo : (j : Fin k) -> from (to j) = j+        fromTo {k = S k} FZ = rewrite strengthenLast k in Refl+        fromTo (FS x) = rewrite strengthenWeaken x in Refl+||| Sends `last` to `FZ` and every other `x` to `FS x`.+rotatedUp : Iso (Fin n) (Fin n)+rotatedUp = isoSym rotatedDown

@@ -0,0 +1,155 @@+module Control.Isomorphism.Vect++import Control.Isomorphism+import Data.Vect+import Interfaces.Verified++%default total+%access public export++||| `Vect Z a` has only one value: `[]`.+nilUnit : Iso (Vect Z a) ()+nilUnit = MkIso (const ()) (const []) (\() => Refl) (\[] => Refl)++||| A `Vect (S Z) a` is just an `a`.+oneIdentity : Iso (Vect (S Z) a) a+oneIdentity = MkIso to (\x => [x]) (\x => Refl) (\[x] => Refl)+  where to : Vect 1 a -> a+        to [x] = x++||| Moves between `x :: xs` and `(x, xs)`.+consPair : Iso (Vect (S n) a) (a, Vect n a)+consPair = MkIso to (uncurry (::)) (\(x, xs) => Refl) (\(x :: xs) => Refl)+  where to : Vect (S n) a -> (a, Vect n a)+        to (x :: xs) = (x, xs)++||| An `Iso` based on `splitAt` and `(++)`.+splitPair : Iso (Vect (n + m) a) (Vect n a, Vect m a)+splitPair {n} {m} = MkIso (splitAt n) (uncurry (++)) toFrom fromTo+  where pairify : q = w -> e = r -> (q, e) = (w, r)+        pairify Refl Refl = Refl+        toFrom (ns, ms) = trans (splitAtTakeDrop n (ns ++ ms)) $ pairify (takePrefix ns ms) (dropPrefix ns ms)+        fromTo xs = rewrite splitAtTakeDrop {m} n xs in takeDropConcat n xs++||| An `Iso` based on `zip` and `unzip`.+zipped : Iso (Vect n a, Vect n b) (Vect n (a, b))+zipped = MkIso (uncurry zip) unzip toFrom (\(as, bs) => fromTo as bs)+  where toFrom : {n : Nat} -> (xs : Vect n (a, b)) -> uncurry Vect.zip (unzip xs) = xs+        toFrom [] = Refl+        toFrom ((a, b) :: xs) with (unzip xs) proof p+          | (as, bs) = cong $ trans (cong p) (toFrom xs)+        fromTo : {n : Nat} -> (as : Vect n a) -> (bs : Vect n b) -> unzip (zip as bs) = (as, bs)+        fromTo [] [] = Refl+        fromTo (a :: as) (b :: bs) = rewrite fromTo as bs in Refl++||| An `Iso` based on `zip3` and `unzip3`.+zipped3 : Iso (Vect n a, Vect n b, Vect n c) (Vect n (a, b, c))+zipped3 = MkIso (uncurrry zip3) unzip3 toFrom (\(as, bs, cs) => fromTo as bs cs)+  where uncurrry : (w -> x -> y -> z) -> ((w, x, y) -> z)+        uncurrry w (x, y, z) = w x y z+        toFrom : {n : Nat} -> (xs : Vect n (a, b, c)) -> uncurrry Vect.zip3 (unzip3 xs) = xs+        toFrom [] = Refl+        toFrom ((a, b, c) :: xs) with (unzip3 xs) proof p+          | (as, bs, cs) = cong $ trans (cong p) (toFrom xs)+        fromTo : {n : Nat} -> (as : Vect n a) -> (bs : Vect n b) -> (cs : Vect n c) -> unzip3 (zip3 as bs cs) = (as, bs, cs)+        fromTo [] [] [] = Refl+        fromTo (a :: as) (b :: bs) (c :: cs) = rewrite fromTo as bs cs in Refl++||| An `Iso` based on `transpose`.+transposition : Iso (Vect o (Vect i a)) (Vect i (Vect o a))+transposition {a} = MkIso transpose transpose prf prf+  where prf : {i : Nat} -> {o : Nat} -> (xss : Vect o (Vect i a)) -> transpose (transpose xss) = xss+        prf [] = vectMustBeNil $ transpose [| [] |]+        prf (xs :: xss) = rewrite transposeCons xs (transpose xss) in cong (prf xss)++||| Split the `Vect` every `m` elements, making `n` `Vect m a`s.+||| The result is rectangular and has the same order as the original.+|||+||| This is the inverse of `concat`.+unconcat : Vect (n * m) a -> Vect n (Vect m a)+unconcat {n = Z} [] = []+unconcat {n = S k} {m} xs with (splitAt m xs)+  | (xs', xss) = xs' :: unconcat xss+||| An `Iso` based on `unconcat` and `concat`.+|||+||| ```idris example+||| from rectangular [[1,2,3],[4,5,6]]+||| ```+rectangular : Iso (Vect (n * m) a) (Vect n (Vect m a))+rectangular = MkIso unconcat concat toFrom fromTo+  where toFrom : (xss : Vect i (Vect o a)) -> unconcat (concat xss) = xss+        toFrom {i = Z} [] = Refl+        toFrom {i = S i} {o} (xs :: xss) = rewrite splitAtTakeDrop o {m = i * o} (xs ++ concat xss) in+                                           rewrite takePrefix xs (concat xss) in+                                           rewrite dropPrefix xs (concat xss) in+                                           cong (toFrom xss)+        fromTo : (xs : Vect (i * o) a) -> concat (unconcat xs) = xs+        fromTo {i = Z} [] = Refl+        fromTo {i = S i} {o} xs = rewrite splitAtTakeDrop o {m = i * o} xs in+                                  rewrite fromTo {i} {o} (drop o xs) in+                                  takeDropConcat o xs++-- Not an Iso because (=) is not extensional, but it works in spirit+||| Go through all possible inputs and tabulate the outputs in a `Vect`.+|||+||| Or: turn a function from indices to values into a `Vect`.+||| Or: the inverse of `index`.+unindex : (Fin n -> a) -> Vect n a+unindex {n = Z} _ = []+unindex {n = S k} f = f FZ :: unindex (f . FS)++||| Indexing into the table of outputs of `f` is like calling `f` itself.+indexUnindex : (i : Fin n) -> (f : Fin n -> a) -> index i (unindex f) = f i+indexUnindex FZ _ = Refl+indexUnindex (FS k) f = rewrite indexUnindex k (f . FS) in Refl+||| Given a function `f`, a `Vect` `xs`, and a proof that calling `f` gives the same result as indexing into `xs`,+||| prove that `xs` is the table of outputs of `f`.+unindexIndex' : (xs : Vect n a) -> (f : Fin n -> a) -> ((i : Fin n) -> f i = index i xs) -> unindex f = xs+unindexIndex' [] _ _ = Refl+unindexIndex' (x :: xs) f prf = rewrite prf FZ in rewrite unindexIndex' xs (f . FS) (\i => rewrite prf $ FS i in Refl) in Refl+||| If `f` and `g` are extensionally equal (equal outputs for all inputs), then `unindex f = unindex g`.+congExtUnindex : (f : Fin n -> a) -> (g : Fin n -> a) -> ((i : Fin n) -> f i = g i) -> unindex f = unindex g+congExtUnindex f g p = unindexIndex' (unindex g) f $ \i => trans (p i) $ sym $ indexUnindex i g+||| Functions with the same tables are the same themselves.+injExtUnindex : (f : Fin n -> a) -> (g : Fin n -> a) -> unindex f = unindex g -> ((i : Fin n) -> f i = g i)+injExtUnindex f g p i = rewrite sym $ indexUnindex i f in rewrite sym $ indexUnindex i g in cong p+||| A simpler version of `unindexIndex'` which only proves that `unindex` is the inverse of `index`.+unindexIndex : (xs : Vect n a) -> unindex (\i => index i xs) = xs+unindexIndex xs = unindexIndex' xs (\i => index i xs) (\i => Refl)++||| Given a function that computes an index in the input from the index in the output, produce a `Vect o` of elements from the input.+|||+||| This is the map function of the functor `\i => Vect i a` from `\i, o => Fin o -> Fin i` to `\i, o => Vect i a -> Vect o a`.+fromIndices : (Fin o -> Fin i) -> Vect i a -> Vect o a+fromIndices f xs = unindex (flip index xs . f)+indexFromIndices : (f : Fin o -> Fin i) -> (xs : Vect i a) -> (n : Fin o) -> index n (fromIndices f xs) = index (f n) xs+indexFromIndices f xs n = indexUnindex n (\i => index (f i) xs)+fromIndicesFromIndices : (to : Fin n -> Fin n) -> (from : Fin n -> Fin n) -> (fromTo : (i : Fin n) -> from (to i) = i) -> (xs : Vect n a) -> fromIndices to (fromIndices from xs) = xs+fromIndicesFromIndices to from fromTo xs = unindexIndex' xs (\x => index (to x) (unindex (\x' => index (from x') xs))) $ \i =>+                        rewrite indexUnindex (to i) (\x' => index (from x') xs) in rewrite fromTo i in Refl++||| Given a permutation of the indices, provide an `Iso` that can permute a `Vect n` the "same" way. More precisely,+||| if the index `i` is sent to `j`, then the element at index `i` ends up at index `j` (`indexPermuted`). An+||| `Iso (Fin n) (Fin n)` represents a permutation of the integers `[0, n)` because it ensures that no elements+||| are "lost" or "duplicated".+|||+||| Note this has the *opposite* behavior to `fromIndices`. This function is more "visceral"; it can be imagined+||| as shuffling a `Vect` in the same way `map (to permutation)` shuffles `range`. Or, in more categorical terms,+||| `fromIndices` represents a contravariant functor from the category `\i, o => Fin i -> Fin o` to `\i, o => Vect i a -> Vect o a`,+||| and `permuted` represents that functor restricted to isomorphisms and made covariant with `isoSym`.+|||+||| ```idris example+||| to (permuted (stimes 2 rotatedDown)) [1, 2, 3, 4, 5] == [3, 4, 5, 1, 2]+||| to (permuted (swapped 3 0))          [1, 2, 3, 4, 5] == [4, 2, 3, 1, 5]+||| ```+|||+||| @ permutation an `Iso` representing the transformation on the indices+permuted : (permutation : Iso (Fin n) (Fin n)) -> Iso (Vect n a) (Vect n a)+-- [to, from => f from, f to] is not a typo+-- fromIndices needs a function outputIdx => inputIdx, so to "align" the "motion" of the Fins with the elements, to uses from and from uses to.+permuted (MkIso toI fromI toFromI fromToI) = MkIso (fromIndices fromI) (fromIndices toI) (fromIndicesFromIndices fromI toI toFromI) (fromIndicesFromIndices toI fromI fromToI)+permutedSym : (permutation : Iso (Fin n) (Fin n)) -> permuted (isoSym permutation) = isoSym (permuted permutation)+permutedSym (MkIso to from toFrom fromTo) = Refl+indexPermuted : (permutation : Iso (Fin n) (Fin n)) -> (i : Fin n) -> (xs : Vect n a) -> index i xs = index (to permutation i) (to (permuted permutation) xs)+indexPermuted (MkIso to from toFrom fromTo) i xs = replace {P = \xs' => index i xs' = index (to i) (fromIndices from xs) } (fromIndicesFromIndices to from fromTo xs) $+                                                   rewrite indexFromIndices to (fromIndices from xs) i in Refl

@@ -4,6 +4,6 @@  ||| 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 : (n : Fin m) -> LT (finToNat n) m+elemSmallerThanBound FZ = LTESucc LTEZero elemSmallerThanBound (FS x) = LTESucc (elemSmallerThanBound x)

@@ -0,0 +1,8 @@+module Data.Nat++%default total++diff : Nat -> Nat -> Nat+diff k Z = k+diff Z j = j+diff (S k) (S j) = diff k j

@@ -4,8 +4,10 @@ import Control.Algebra.Lattice import Control.Algebra.NumericImplementations import Control.Algebra.VectorSpace+import Data.Vect import Data.ZZ +%default total %access public export  -- Due to these being basically unused and difficult to implement,@@ -16,17 +18,42 @@ -- and Monoid).  interface Functor f => VerifiedFunctor (f : Type -> Type) where-  functorIdentity : {a : Type} -> (x : f a) -> map Basics.id x = Basics.id x+  functorIdentity : {a : Type} -> (g : a -> a) -> ((v : a) -> g v = v) -> (x : f a) -> map g x = x   functorComposition : {a : Type} -> {b : Type} -> (x : f a) ->                        (g1 : a -> b) -> (g2 : b -> c) ->                        map (g2 . g1) x = (map g2 . map g1) x +functorIdentity' : VerifiedFunctor f => (x : f a) -> map Basics.id x = x+functorIdentity' {f} = functorIdentity {f} id (\x => Refl)++VerifiedFunctor (Pair a) where+  functorIdentity g p (a,b) = rewrite p b in Refl+  functorComposition (a,b) g1 g2 = Refl++VerifiedFunctor (Either a) where+  functorIdentity _ _ (Left _) = Refl+  functorIdentity _ p (Right x) = cong (p x)+  functorComposition (Left _) _ _ = Refl+  functorComposition (Right _) _ _ = Refl+ VerifiedFunctor Maybe where-  functorIdentity Nothing = Refl-  functorIdentity (Just x) = Refl+  functorIdentity _ _ Nothing = Refl+  functorIdentity g p (Just x) = rewrite p x in Refl   functorComposition Nothing g1 g2 = Refl   functorComposition (Just x) g1 g2 = Refl +VerifiedFunctor List where+  functorIdentity _ _ [] = Refl+  functorIdentity g p (x :: xs) = rewrite p x in cong (functorIdentity g p xs)+  functorComposition [] _ _ = Refl+  functorComposition (x :: xs) f g = rewrite functorComposition xs f g in Refl++VerifiedFunctor (Vect n) where+  functorIdentity _ _ [] = Refl+  functorIdentity g p (x :: xs) = rewrite p x in cong (functorIdentity g p xs)+  functorComposition [] _ _ = Refl+  functorComposition (x :: xs) f g = rewrite functorComposition xs f g in Refl+ interface (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where   applicativeMap : (x : f a) -> (g : a -> b) ->                    map g x = pure g <*> x@@ -38,6 +65,90 @@   applicativeInterchange : (x : a) -> (g : f (a -> b)) ->                            g <*> pure x = pure (\g' : (a -> b) => g' x) <*> g +VerifiedApplicative (Either a) where+  applicativeMap (Left x) g = Refl+  applicativeMap (Right x) g = Refl+  applicativeIdentity (Left x) = Refl+  applicativeIdentity (Right x) = Refl+  applicativeComposition (Left x) (Left y) (Left z) = Refl+  applicativeComposition (Left x) (Left y) (Right z) = Refl+  applicativeComposition (Left x) (Right y) (Left z) = Refl+  applicativeComposition (Left x) (Right y) (Right z) = Refl+  applicativeComposition (Right x) (Left y) (Left z) = Refl+  applicativeComposition (Right x) (Left y) (Right z) = Refl+  applicativeComposition (Right x) (Right y) (Left z) = Refl+  applicativeComposition (Right x) (Right y) (Right z) = Refl+  applicativeHomomorphism x g = Refl+  applicativeInterchange x (Left y) = Refl+  applicativeInterchange x (Right y) = Refl+  +private+foldrConcatEq : (g1 : List (a -> b)) -> (g2 : List (a -> b)) ->+                (xs : List a) ->+                foldr (\f, meth => map f xs ++ meth) [] (g1 ++ g2) = foldr (\f, meth => map f xs ++ meth) [] g1 ++ foldr (\f, meth => map f xs ++ meth) [] g2+foldrConcatEq [] _ _ = Refl+foldrConcatEq (g1 :: gs1) gs2 xs =+  trans+    (cong $ foldrConcatEq gs1 gs2 xs)+    (appendAssociative+      (map g1 xs)+      (foldr (\f, meth => map f xs ++ meth) [] gs1)+      (foldr (\f, meth => map f xs ++ meth) [] gs2))++private+foldrConcatEq' : (x1 : List a) -> (x2 : List a) ->+                 (g : a -> List b) ->+                 foldr (\x, meth => g x ++ meth) [] (x1 ++ x2) = foldr (\x, meth => g x ++ meth) [] x1 ++ foldr (\x, meth => g x ++ meth) [] x2+foldrConcatEq' [] _ _ = Refl+foldrConcatEq' (x1 :: xs1) xs2 g =+  trans+    (cong {f=((++) $ g x1)} $ foldrConcatEq' xs1 xs2 g)+    (appendAssociative+      (g x1)+      (foldr (\x, meth => g x ++ meth) [] xs1)+      (foldr (\x, meth => g x ++ meth) [] xs2))++private+foldrMapCombine : (xs : List a) -> (gs1 : List (a -> b)) -> (g2 : b -> c) ->+                  map g2 (foldr (\g, meth => map g xs ++ meth) [] gs1) =+                  foldr (\g, meth => map g xs ++ meth) [] (map ((.) g2) gs1)+foldrMapCombine xs [] g2 = Refl+foldrMapCombine xs (g1 :: gs1) g2 =+  trans+    (mapAppendDistributive g2 (map g1 xs) (foldr (\g, meth => map g xs ++ meth) [] gs1))+    (appendCong2 (sym $ functorComposition xs g1 g2) (foldrMapCombine xs gs1 g2))++VerifiedApplicative List where+  applicativeMap [] f = Refl+  applicativeMap (x :: xs) f = rewrite applicativeMap xs f in Refl+  applicativeIdentity xs = rewrite sym $ applicativeMap xs id in functorIdentity' xs+  applicativeComposition _ _ [] = Refl+  applicativeComposition xs gs1 (g2 :: gs2) = trans+    (trans+      (foldrConcatEq (map ((.) g2) gs1) (foldr (\g, meth => map g gs1 ++ meth) [] (map (.) gs2 ++ [])) xs)+      (cong $ applicativeComposition xs gs1 gs2))+    (sym $+      cong {f=(++ foldr (\g, meth => map g (foldr (\g', meth' => map g' xs ++ meth') [] gs1) ++ meth) [] gs2)} $+        foldrMapCombine xs gs1 g2)+  applicativeHomomorphism x g = Refl+  applicativeInterchange x [] = Refl+  applicativeInterchange x (g :: gs) = cong $ applicativeInterchange x gs++VerifiedApplicative (Vect n) where+  applicativeMap [] f = Refl+  applicativeMap (x :: xs) f = rewrite applicativeMap xs f in Refl+  applicativeIdentity xs = rewrite sym $ applicativeMap xs id in functorIdentity' xs+  applicativeComposition [] [] [] = Refl+  applicativeComposition (x :: xs) (f :: fs) (g :: gs) = rewrite applicativeComposition xs fs gs in Refl+  applicativeHomomorphism = prf+    where prf : with Vect ((x : a) -> (f : a -> b) -> zipWith Basics.apply (replicate m f) (replicate m x) = replicate m (f x))+          prf {m = Z} x f = Refl+          prf {m = S k} x f = rewrite prf {m = k} x f in Refl+  applicativeInterchange = prf+    where prf : with Vect ((x : a) -> (f : Vect m (a -> b)) -> zipWith Basics.apply f (replicate m x) = zipWith Basics.apply (replicate m (\f' => f' x)) f)+          prf {m = Z} x [] = Refl+          prf {m = S k} x (f :: fs) = rewrite prf x fs in Refl+ VerifiedApplicative Maybe where   applicativeMap Nothing g = Refl   applicativeMap (Just x) g = Refl@@ -65,19 +176,64 @@   monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->                        (mx >>= f) >>= g = mx >>= (\x => f x >>= g) +VerifiedMonad (Either a) where+  monadApplicative (Left x) (Left y) = Refl+  monadApplicative (Left x) (Right y) = Refl+  monadApplicative (Right x) (Left y) = Refl+  monadApplicative (Right x) (Right y) = Refl+  monadLeftIdentity x f = Refl+  monadRightIdentity (Left x) = Refl+  monadRightIdentity (Right x) = Refl+  monadAssociativity (Left x) f g = Refl+  monadAssociativity (Right x) f g = Refl+ VerifiedMonad Maybe where-    monadApplicative Nothing Nothing = Refl-    monadApplicative Nothing (Just x) = Refl-    monadApplicative (Just x) Nothing = Refl-    monadApplicative (Just x) (Just y) = Refl-    monadLeftIdentity x f = Refl-    monadRightIdentity Nothing = Refl-    monadRightIdentity (Just x) = Refl-    monadAssociativity Nothing f g = Refl-    monadAssociativity (Just x) f g = Refl+  monadApplicative Nothing Nothing = Refl+  monadApplicative Nothing (Just x) = Refl+  monadApplicative (Just x) Nothing = Refl+  monadApplicative (Just x) (Just y) = Refl+  monadLeftIdentity x f = Refl+  monadRightIdentity Nothing = Refl+  monadRightIdentity (Just x) = Refl+  monadAssociativity Nothing f g = Refl+  monadAssociativity (Just x) f g = Refl +VerifiedMonad List where+  monadApplicative [] _ = Refl+  monadApplicative (x :: xs) [] = Refl+  monadApplicative (g :: gs) xs = appendCong2 (mapFoldrEq g xs) (monadApplicative gs xs) where+    mapFoldrEq : (f : a -> b) -> (x : List a) -> map f x = foldr (\x1, meth => f x1 :: meth) [] x+    mapFoldrEq _ [] = Refl+    mapFoldrEq f (_ :: x) = cong $ mapFoldrEq f x+  monadLeftIdentity x f = appendNilRightNeutral (f x)+  monadRightIdentity [] = Refl+  monadRightIdentity (x :: xs) = cong $ monadRightIdentity xs+  monadAssociativity [] _ _ = Refl+  monadAssociativity (x :: xs) g1 g2 =+    trans+      (foldrConcatEq' (g1 x) (foldr (\x1, meth => g1 x1 ++ meth) [] xs) g2)+      (cong $ monadAssociativity xs g1 g2)++interface (Alternative f, VerifiedApplicative f) => VerifiedAlternative (f : Type -> Type) where+  alternativeLeftIdentity : (x : f a) -> Applicative.empty <|> x = x+  alternativeRightIdentity : (x : f a) -> x <|> Applicative.empty = x+  alternativeAssociativity : (x : f a) -> (y : f a) -> (z : f a) ->+                             x <|> (y <|> z) = (x <|> y) <|> z++VerifiedAlternative Maybe where+  alternativeLeftIdentity _ = Refl+  alternativeRightIdentity Nothing = Refl+  alternativeRightIdentity (Just _) = Refl+  alternativeAssociativity Nothing _ _ = Refl+  alternativeAssociativity (Just _) _ _ = Refl++VerifiedAlternative List where+  alternativeLeftIdentity _ = Refl+  alternativeRightIdentity = appendNilRightNeutral+  alternativeAssociativity = appendAssociative+ interface Semigroup a => VerifiedSemigroup a where-  total semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r+  semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r  implementation VerifiedSemigroup (List a) where   semigroupOpIsAssociative = appendAssociative@@ -95,8 +251,8 @@   semigroupOpIsAssociative = multAssociativeZ  interface (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where-  total monoidNeutralIsNeutralL : (l : a) -> l <+> Algebra.neutral = l-  total monoidNeutralIsNeutralR : (r : a) -> Algebra.neutral <+> r = r+  monoidNeutralIsNeutralL : (l : a) -> l <+> Algebra.neutral = l+  monoidNeutralIsNeutralR : (r : a) -> Algebra.neutral <+> r = r  [PlusNatMonoidV] VerifiedMonoid Nat using PlusNatSemiV, PlusNatMonoid where    monoidNeutralIsNeutralL = plusZeroRightNeutral@@ -119,8 +275,8 @@   monoidNeutralIsNeutralR xs = Refl  interface (VerifiedMonoid a, Group a) => VerifiedGroup a where-  total groupInverseIsInverseL : (l : a) -> l <+> inverse l = Algebra.neutral-  total groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral+  groupInverseIsInverseL : (l : a) -> l <+> inverse l = Algebra.neutral+  groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral  VerifiedGroup ZZ using PlusZZMonoidV where   groupInverseIsInverseL k = rewrite sym $ multCommutativeZ (NegS 0) k in@@ -133,15 +289,15 @@                              plusNegateInverseRZ k  interface (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where-  total abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l+  abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l  VerifiedAbelianGroup ZZ where   abelianGroupOpIsCommutative = plusCommutativeZ  interface (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where-  total ringOpIsAssociative   : (l, c, r : a) -> l <.> (c <.> r) = (l <.> c) <.> r-  total ringOpIsDistributiveL : (l, c, r : a) -> l <.> (c <+> r) = (l <.> c) <+> (l <.> r)-  total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)+  ringOpIsAssociative   : (l, c, r : a) -> l <.> (c <.> r) = (l <.> c) <.> r+  ringOpIsDistributiveL : (l, c, r : a) -> l <.> (c <+> r) = (l <.> c) <+> (l <.> r)+  ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)  VerifiedRing ZZ where   ringOpIsAssociative = multAssociativeZ@@ -149,19 +305,19 @@   ringOpIsDistributiveR = multDistributesOverPlusLeftZ  interface (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where-  total ringWithUnityIsUnityL : (l : a) -> l <.> Algebra.unity = l-  total ringWithUnityIsUnityR : (r : a) -> Algebra.unity <.> r = r+  ringWithUnityIsUnityL : (l : a) -> l <.> Algebra.unity = l+  ringWithUnityIsUnityR : (r : a) -> Algebra.unity <.> r = r  VerifiedRingWithUnity ZZ where   ringWithUnityIsUnityL = multOneRightNeutralZ   ringWithUnityIsUnityR = multOneLeftNeutralZ  interface JoinSemilattice a => VerifiedJoinSemilattice a where-  total joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r-  total joinSemilatticeJoinIsCommutative : (l, r : a)    -> join l r = join r l-  total joinSemilatticeJoinIsIdempotent  : (e : a)       -> join e e = e+  joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r+  joinSemilatticeJoinIsCommutative : (l, r : a)    -> join l r = join r l+  joinSemilatticeJoinIsIdempotent  : (e : a)       -> join e e = e  interface MeetSemilattice a => VerifiedMeetSemilattice a where-  total meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r-  total meetSemilatticeMeetIsCommutative : (l, r : a)    -> meet l r = meet r l-  total meetSemilatticeMeetIsIdempotent  : (e : a)       -> meet e e = e+  meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r+  meetSemilatticeMeetIsCommutative : (l, r : a)    -> meet l r = meet r l+  meetSemilatticeMeetIsIdempotent  : (e : a)       -> meet e e = e

@@ -160,6 +160,16 @@ hexDigits : Lexer hexDigits = some hexDigit +||| Recognise a single octal digit+||| /[0-8]/+octDigit : Lexer+octDigit = pred isHexDigit++||| Recognise one or more octal digits+||| /[0-8]+/+octDigits : Lexer+octDigits = some hexDigit+ ||| Recognise a single alpha character ||| /[A-Za-z]/ alpha : Lexer@@ -269,7 +279,21 @@ ||| /'(\\\\.|[\^'])'/ charLit : Lexer charLit = let q = '\'' in-              is q <+> (escape '\\' any <|> isNot q) <+> is q+              is q <+> (escape '\\' (control <|> any) <|> isNot q) <+> is q+  where+    lexStr : List String -> Lexer+    lexStr [] = fail+    lexStr (t :: ts) = exact t <|> lexStr ts++    control : Lexer+    control = lexStr ["NUL", "SOH", "STX", "ETX", "EOT", "ENQ", "ACK", "BEL",+                      "BS",  "HT",  "LF",  "VT",  "FF",  "CR",  "SO",  "SI",+                      "DLE", "DC1", "DC2", "DC3", "DC4", "NAK", "SYN", "ETB",+                      "CAN", "EM",  "SUB", "ESC", "FS",  "GS",  "RS",  "US",+                      "SP",  "DEL"]+                <|> (is 'x' <+> hexDigits)+                <|> (is 'o' <+> octDigits)+                <|> digits  ||| Recognise an integer literal (possibly with a '-' prefix) ||| /-?[0-9]+/

@@ -82,7 +82,7 @@  strIndex : StrLen -> Nat -> Maybe Char strIndex (MkStrLen str len) i-    = if i >= len then Nothing+    = if cast {to = Integer} i >= cast len then Nothing                   else Just (assert_total (prim__strIndex str (cast i)))  mkStr : String -> StrLen

@@ -118,7 +118,7 @@ ||| list of values from `p`, along with a proof that the resulting list is ||| non-empty. someTill' : {c : Bool} ->-            (end : Grammar tok c a) ->+            (end : Grammar tok c e) ->             (p : Grammar tok True a) ->             Grammar tok True (xs : List a ** NonEmpty xs) someTill' end p

@@ -145,9 +145,9 @@  ||| Use the Wadler-Leijen algorithm to pretty print the `doc`. ||| The algorithm uses a page width of `width` and a ribbon-||| width of `(ribbonfrac * width)` characters. The ribbon width is+||| width of `(rfrac * width)` characters. The ribbon width is ||| the maximal amount of non-indentation characters on a line. The-||| parameter `ribbonfrac` should be between `0.0` and `1.0`. If it is+||| parameter `rfrac` should be between `0.0` and `1.0`. If it is ||| lower or higher, the ribbon width will be 0 or `width` ||| respectively. render : (rfrac : Double)

@@ -12,7 +12,12 @@         , Control.Algebra.VectorSpace          , Control.Delayed++        , Control.Isomorphism.Extra+        , Control.Isomorphism.Fin         , Control.Isomorphism.Primitives+        , Control.Isomorphism.Vect+         , Control.Monad.Syntax         , Control.Partial         , Control.Pipeline@@ -43,6 +48,7 @@         , Data.Matrix.Algebraic         , Data.Matrix.Numeric +        , Data.Nat         , Data.Nat.Parity         , Data.Nat.DivMod         , Data.Nat.DivMod.IteratedSubtraction

@@ -206,6 +206,7 @@ %extern prim__stderr : Ptr  %extern prim__null : Ptr+%extern prim__managedNull : ManagedPtr %extern prim__eqPtr : Ptr -> Ptr -> Int %extern prim__eqManagedPtr : ManagedPtr -> ManagedPtr -> Int %extern prim__registerPtr : Ptr -> Int -> ManagedPtr

@@ -157,8 +157,10 @@   -- For the primitives, we have to cheat because we don't have access to their--- internal implementations. We postulate the inequality proofs because we're--- never going to have to compute anything from them.+-- internal implementations. We use believe_me for the inequality proofs +-- because we don't them to reduce (and they should never be needed anyway...)+-- A postulate would be better, but erasure analysis may think they're needed+-- for computation in a higher order setting.  -------------------------------------------------------------------------------- -- Int@@ -170,7 +172,8 @@                      False => No primitiveNotEq        where primitiveEq : x = y              primitiveEq = really_believe_me (Refl {x})-             postulate primitiveNotEq : x = y -> Void+             primitiveNotEq : x = y -> Void+             primitiveNotEq prf = believe_me {b = Void} ()  -------------------------------------------------------------------------------- -- Char@@ -182,7 +185,8 @@                      False => No primitiveNotEq        where primitiveEq : x = y              primitiveEq = really_believe_me (Refl {x})-             postulate primitiveNotEq : x = y -> Void+             primitiveNotEq : x = y -> Void+             primitiveNotEq prf = believe_me {b = Void} ()  -------------------------------------------------------------------------------- -- Integer@@ -194,7 +198,8 @@                      False => No primitiveNotEq        where primitiveEq : x = y              primitiveEq = really_believe_me (Refl {x})-             postulate primitiveNotEq : x = y -> Void+             primitiveNotEq : x = y -> Void+             primitiveNotEq prf = believe_me {b = Void} ()  -------------------------------------------------------------------------------- -- String@@ -206,7 +211,8 @@                      False => No primitiveNotEq        where primitiveEq : x = y              primitiveEq = really_believe_me (Refl {x})-             postulate primitiveNotEq : x = y -> Void+             primitiveNotEq : x = y -> Void+             primitiveNotEq prf = believe_me {b = Void} ()  -------------------------------------------------------------------------------- -- Ptr@@ -218,7 +224,8 @@                      False => No primitiveNotEq        where primitiveEq : x = y              primitiveEq = really_believe_me (Refl {x})-             postulate primitiveNotEq : x = y -> Void+             primitiveNotEq : x = y -> Void+             primitiveNotEq prf = believe_me {b = Void} ()  -------------------------------------------------------------------------------- -- ManagedPtr@@ -230,4 +237,5 @@                      False => No primitiveNotEq        where primitiveEq : x = y              primitiveEq = really_believe_me (Refl {x})-             postulate primitiveNotEq : x = y -> Void+             primitiveNotEq : x = y -> Void+             primitiveNotEq prf = believe_me {b = Void} ()

@@ -18,7 +18,6 @@ interface Semigroup ty where   (<+>) : ty -> ty -> ty - ||| Sets equipped with a single binary operation that is associative, along with ||| a neutral element for that binary operation.  Must satisfy the following ||| laws:@@ -30,4 +29,3 @@ |||     forall a,     neutral <+> a   == a interface Semigroup ty => Monoid ty where   neutral : ty-

@@ -87,6 +87,10 @@ maybeToEither def (Just j) = Right j maybeToEither def Nothing  = Left  def +||| Convert an Either to a Maybe from Right injection+eitherToMaybe : Either e a -> Maybe a+eitherToMaybe (Left _) = Nothing+eitherToMaybe (Right x) = Just x  -------------------------------------------------------------------------------- -- Implementations

@@ -375,3 +375,9 @@ changeDir dir      = do ok <- foreign FFI_C "idris_chdir" (String -> IO Int) dir          pure (ok == 0)++export+currentDir : IO String+currentDir = do+  MkRaw s <- foreign FFI_C "idris_currentDir" (IO (Raw String))+  pure s

@@ -675,13 +675,18 @@     (chunk, [])          => [chunk]     (chunk, (c :: rest)) => chunk :: split p (assert_smaller xs rest) -||| A tuple where the first element is a List of the n first elements and-||| the second element is a List of the remaining elements of the list-||| It is equivalent to (take n xs, drop n xs)+||| A tuple where the first element is a `List` of the `n` first elements and+||| the second element is a `List` of the remaining elements of the original.+||| It is equivalent to `(take n xs, drop n xs)` (`splitAtTakeDrop`),+||| but is more efficient.+||| ||| @ n   the index to split at-||| @ xs  the list to split in two+||| @ xs  the `List` to split in two splitAt : (n : Nat) -> (xs : List a) -> (List a, List a)-splitAt n xs = (take n xs, drop n xs)+splitAt Z xs = ([], xs)+splitAt (S k) [] = ([], [])+splitAt (S k) (x :: xs) with (splitAt k xs)+  | (tk, dr) = (x :: tk, dr)  ||| The partition function takes a predicate a list and returns the pair of ||| lists of elements which do and do not satisfy the predicate, respectively;@@ -857,9 +862,33 @@ --------------------------------------------------------------------------------  ||| (::) is injective-consInjective : (x :: xs) = (y :: ys) -> (x = y, xs = ys)+consInjective : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->+                (x :: xs) = (y :: ys) -> (x = y, xs = ys) consInjective Refl = (Refl, Refl) +||| Two lists are equal, if their heads are equal and their tails are equal.+consCong2 : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->+            x = y -> xs = ys -> x :: xs = y :: ys+consCong2 Refl Refl = Refl++||| Appending pairwise equal lists gives equal lists+appendCong2 : {x1 : List a} -> {x2 : List a} ->+              {y1 : List b} -> {y2 : List b} ->+              x1 = y1 -> x2 = y2 -> x1 ++ x2 = y1 ++ y2+appendCong2 {x1=[]} {y1=(_ :: _)} Refl _ impossible+appendCong2 {x1=(_ :: _)} {y1=[]} Refl _ impossible+appendCong2 {x1=[]} {y1=[]} _ eq2 = eq2+appendCong2 {x1=(_ :: _)} {y1=(_ :: _)} eq1 eq2 =+  consCong2+    (fst $ consInjective eq1)+    (appendCong2 (snd $ consInjective eq1) eq2)++||| List.map is distributive over appending.+mapAppendDistributive : (f : a -> b) -> (x : List a) -> (y : List a) ->+                        map f (x ++ y) = map f x ++ map f y+mapAppendDistributive _ [] _ = Refl+mapAppendDistributive f (_ :: xs) y = cong $ mapAppendDistributive f xs y+ ||| The empty list is a right identity for append. appendNilRightNeutral : (l : List a) ->   l ++ [] = l@@ -931,3 +960,12 @@ foldlMatchesFoldr : (f : b -> a -> b) -> (q : b) -> (xs : List a) -> foldl f q xs = foldlAsFoldr f q xs foldlMatchesFoldr f q [] = Refl foldlMatchesFoldr f q (x :: xs) = foldlMatchesFoldr f (f q x) xs++splitAtTakeDrop : (n : Nat) -> (xs : List a) -> splitAt n xs = (take n xs, drop n xs)+splitAtTakeDrop Z xs = Refl+splitAtTakeDrop (S k) [] = Refl+splitAtTakeDrop (S k) (x :: xs) with (splitAt k xs) proof p+  | (tk, dr) = let prf = trans p (splitAtTakeDrop k xs)+                in aux (cong {f=(x ::) . fst} prf) (cong {f=snd} prf)+  where aux : {a, b : Type} -> {w, x : a} -> {y, z : b} -> w = x -> y = z -> (w, y) = (x, z)+        aux Refl Refl = Refl

@@ -146,6 +146,9 @@ null : Ptr null = prim__null +managedNull : ManagedPtr+managedNull = prim__managedNull+ -- Some more complex string operations  data StrM : String -> Type where@@ -397,6 +400,11 @@ nullPtr : Ptr -> IO Bool nullPtr p = do ok <- foreign FFI_C "isNull" (Ptr -> IO Int) p                pure (ok /= 0)++partial+nullManagedPtr : ManagedPtr -> IO Bool+nullManagedPtr p = do ok <- foreign FFI_C "isNull" (ManagedPtr -> IO Int) p+                      pure (ok /= 0)  ||| Check if a supposed string was actually a null pointer partial

@@ -5,6 +5,8 @@ ||| other metric of size. module Prelude.WellFounded +import Builtins+ import Prelude.Nat import Prelude.List import Prelude.Uninhabited@@ -128,3 +130,6 @@  implementation Sized (List a) where   size = length++implementation (Sized a, Sized b) => Sized (Pair a b) where+  size (x,y) = Nat.plus (size x) (size y)

@@ -1,6 +1,6 @@ .\" Manpage for Idris. .\" Contact <> to correct errors or typos.-.TH man 1 "26 May 2018" "1.3.0" "Idris man page"+.TH man 1 "23 October 2018" "1.3.1" "Idris man page" .SH NAME idris -\ a general purpose pure functional programming language with dependent types. .SH SYNOPSIS

@@ -1,28 +1,24 @@ include ../config.mk  OBJS = idris_rts.o idris_heap.o idris_gc.o idris_gmp.o idris_bitstring.o \-       idris_opts.o idris_stats.o idris_utf8.o idris_stdfgn.o mini-gmp.o \+       idris_opts.o idris_stats.o idris_utf8.o idris_stdfgn.o \        idris_buffer.o getline.o idris_net.o HDRS = idris_rts.h idris_heap.h idris_gc.h idris_gmp.h idris_bitstring.h \-       idris_opts.h idris_stats.h mini-gmp.h idris_stdfgn.h idris_net.h \+       idris_opts.h idris_stats.h idris_stdfgn.h idris_net.h \        idris_buffer.h idris_utf8.h getline.h CFLAGS := $(CFLAGS) CFLAGS += $(GMP_INCLUDE_DIR) $(GMP) -DIDRIS_TARGET_OS="\"$(OS)\"" CFLAGS += -DIDRIS_TARGET_TRIPLE="\"$(MACHINE)\"" -# NOTE: This works around glibc 2.11 not declaring pthread_mutexattr_settype-# and PTHREAD_MUTEX_RECURSIVE by default, causing compilation failures on-# Debian 6 and Ubuntu 10.04 LTS.-ifeq ($(OS), unix)-ifneq ($(shell ldd --version | head -n 1 | grep 2.11),)-	CFLAGS += -D_GNU_SOURCE-endif-endif- ifeq ($(OS), windows) 	OBJS += windows/win_utils.o else 	CFLAGS += -fPIC+endif++ifndef IDRIS_GMP+	OBJS += mini-gmp.o+	HDRS += mini-gmp.h endif  LIBTARGET = libidris_rts.a

@@ -6,8 +6,10 @@     uint8_t data[0]; } Buffer; -void* idris_newBuffer(int bytes) {-    Buffer* buf = malloc(sizeof(Buffer) + bytes*sizeof(uint8_t));+VAL idris_newBuffer(VM* vm, int bytes) {+    size_t size = sizeof(Buffer) + bytes*sizeof(uint8_t);++    Buffer* buf = malloc(size);     if (buf == NULL) {         return NULL;     }@@ -15,7 +17,9 @@     buf->size = bytes;     memset(buf->data, 0, bytes); -    return buf;+    void* retbuf = MKMPTR(vm, buf, size);+    free(buf);+    return retbuf; }  void idris_copyBuffer(void* from, int start, int len,

@@ -6,7 +6,7 @@ #include <stdint.h> #include "idris_rts.h" -void* idris_newBuffer(int bytes);+VAL idris_newBuffer(VM* vm, int bytes);  int idris_getBufferSize(void* buffer); 

@@ -3,7 +3,7 @@ #include "idris_rts.h" #include "idris_stats.h" -void _idris__123_runMain_95_0_125_(VM* vm, VAL* oldbase);+void* _idris__123_runMain_95_0_125_(VM* vm, VAL* oldbase);  #ifdef _WIN32 

@@ -697,10 +697,25 @@         char *start = idris_utf8_advance(str_val, offset_val);         char *end = idris_utf8_advance(start, length_val);         size_t sz = end - start;-        String * newstr = allocStr(vm, sz, 0);-        memcpy(newstr->str, start, sz);-        newstr->str[sz] = '\0';-        return (VAL)newstr;++        if (space(vm, sz)) {+            String * newstr = allocStr(vm, sz, 0);+            memcpy(newstr->str, start, sz);+            newstr->str[sz] = '\0';+            return (VAL)newstr;+        } else {+            // Need to copy into an intermediate string before allocating,+            // because if there's no enough space then allocating will move the+            // original string!+            char* cpystr = malloc(sz);+            memcpy(cpystr, start, sz);++            String * newstr = allocStr(vm, sz, 0);+            memcpy(newstr->str, cpystr, sz);+            newstr->str[sz] = '\0';+            free(cpystr);+            return (VAL)newstr;+        }     } } 

@@ -212,7 +212,7 @@  // Functions all take a pointer to their VM, and previous stack base, // and return nothing.-typedef void(*func)(VM*, VAL*);+typedef void*(*func)(VM*, VAL*);  // Register access @@ -282,9 +282,10 @@ #endif  #define INITFRAME TRACE\-                  __attribute__((unused)) VAL* myoldbase+                  __attribute__((unused)) VAL* myoldbase;\+                  void* callres -#define REBASE vm->valstack_base = oldbase+#define REBASE vm->valstack_base = oldbase; return NULL #define RESERVE(x) do { \     if (vm->valstack_top+(x) > vm->stack_max) { stackOverflow(); } \     else { memset(vm->valstack_top, 0, (x)*sizeof(VAL)); } \@@ -293,8 +294,12 @@ #define TOPBASE(x) vm->valstack_top = vm->valstack_base + (x) #define BASETOP(x) vm->valstack_base = vm->valstack_top + (x) #define STOREOLD myoldbase = vm->valstack_base-#define CALL(f) f(vm, myoldbase);-#define TAILCALL(f) f(vm, oldbase);++#define CALL(f) callres = f(vm, myoldbase); \+  while(callres!=NULL) { \+      callres = ((func)(callres))(vm, myoldbase); \+  }+#define TAILCALL(f) return (void*)(f);  // Creating new values (each value placed at the top of the stack) VAL MKFLOAT(VM* vm, double val);

@@ -259,3 +259,11 @@     free(sb);     return str; }++VAL idris_currentDir() {+   char cwd[1024];+   if (getcwd(cwd, sizeof(cwd)) != NULL)+     return MKSTR(get_vm(),cwd);+   else+     return MKSTR(get_vm(),"");+}

@@ -55,4 +55,6 @@  void idris_forceGC(); +VAL idris_currentDir();+ #endif

@@ -117,11 +117,7 @@                   else ["-fwrapv", "-fno-strict-overflow"]  gccDbg DEBUG = ["-g"]--- clang optimises sibling calls in O1, but gcc doesn't--- on the other hand, O1 compiles significantly faster in clang without--- any noticeable performance hit.-gccDbg TRACE = ["-O1", "-foptimize-sibling-calls"]-gccDbg _ = ["-O1", "-foptimize-sibling-calls"]+gccDbg _ = []  cname :: Name -> String cname n = "_idris_" ++ concatMap cchar (showCG n)@@ -137,14 +133,14 @@ creg Tmp = "REG1"  toDecl :: Name -> String-toDecl f = "void " ++ cname f ++ "(VM*, VAL*);\n"+toDecl f = "void* " ++ cname f ++ "(VM*, VAL*);\n"  toC :: Name -> [BC] -> String toC f code     = -- "/* " ++ show code ++ "*/\n\n" ++-      "void " ++ cname f ++ "(VM* vm, VAL* oldbase) {\n" ++-                 indent 1 ++ "INITFRAME;\n" ++-                 concatMap (bcc 1) code ++ "}\n\n"+      "void* " ++ cname f ++ "(VM* vm, VAL* oldbase) {\n" +++                  indent 1 ++ "INITFRAME;\nloop:\n" +++                  concatMap (bcc f 1) code ++ "}\n\n"  showCStr :: String -> String showCStr s = '"' : foldr ((++) . showChar) "\"" s@@ -180,9 +176,9 @@                  2 -> s                  _ -> error $ "Can't happen: String of invalid length " ++ show s -bcc :: Int -> BC -> String-bcc i (ASSIGN l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"-bcc i (ASSIGNCONST l c)+bcc :: Name -> Int -> BC -> String+bcc f i (ASSIGN l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"+bcc f i (ASSIGNCONST l c)     = indent i ++ creg l ++ " = " ++ mkConst c ++ ";\n"   where     mkConst (I i) = "MKINT(" ++ show i ++ ")"@@ -203,10 +199,10 @@     mkConst c | isTypeConst c = "MKINT(42424242)"     mkConst c = error $ "mkConst of (" ++ show c ++ ") not implemented" -bcc i (UPDATE l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"-bcc i (MKCON l loc tag []) | tag < 256+bcc f i (UPDATE l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"+bcc f i (MKCON l loc tag []) | tag < 256     = indent i ++ creg l ++ " = NULL_CON(" ++ show tag ++ ");\n"-bcc i (MKCON l loc tag args)+bcc f i (MKCON l loc tag args)     = indent i ++ alloc loc tag ++       indent i ++ setArgs 0 args ++ "\n" ++       indent i ++ creg l ++ " = " ++ creg Tmp ++ ";\n"@@ -220,21 +216,21 @@             = "updateCon(" ++ creg Tmp ++ ", " ++ creg old ++ ", " ++ show tag ++ ", " ++                     show (length args) ++ ");\n" -bcc i (PROJECT l loc a) = indent i ++ "PROJECT(vm, " ++ creg l ++ ", " ++ show loc +++bcc f i (PROJECT l loc a) = indent i ++ "PROJECT(vm, " ++ creg l ++ ", " ++ show loc ++                                       ", " ++ show a ++ ");\n"-bcc i (PROJECTINTO r t idx)+bcc f i (PROJECTINTO r t idx)     = indent i ++ creg r ++ " = GETARG(" ++ creg t ++ ", " ++ show idx ++ ");\n"-bcc i (CASE True r [(_, alt)] Nothing)+bcc f i (CASE True r [(_, alt)] Nothing)     = indent i ++ showCode i alt   where     showCode :: Int -> [BC] -> String-    showCode i bc = "{\n" ++ concatMap (bcc (i + 1)) bc +++    showCode i bc = "{\n" ++ concatMap (bcc f (i + 1)) bc ++                     indent i ++ "}\n"-bcc i (CASE True r code def)+bcc f i (CASE True r code def)     | length code < 6 && length code > 1 = showCase i def code   where     showCode :: Int -> [BC] -> String-    showCode i bc = "{\n" ++ concatMap (bcc (i + 1)) bc +++    showCode i bc = "{\n" ++ concatMap (bcc f (i + 1)) bc ++                     indent i ++ "}\n"      showCase :: Int -> Maybe [BC] -> [(Int, [BC])] -> String@@ -244,7 +240,7 @@         = indent i ++ "if (CTAG(" ++ creg r ++ ") == " ++ show t ++ ") " ++ showCode i c            ++ indent i ++ "else\n" ++ showCase i def cs -bcc i (CASE safe r code def)+bcc f i (CASE safe r code def)     = indent i ++ "switch(" ++ ctag safe ++ "(" ++ creg r ++ ")) {\n" ++       concatMap (showCase i) code ++       showDef i def ++@@ -254,11 +250,12 @@     ctag False = "TAG"      showCase i (t, bc) = indent i ++ "case " ++ show t ++ ":\n"-                         ++ concatMap (bcc (i+1)) bc ++ indent (i + 1) ++ "break;\n"-    showDef i Nothing = ""+                         ++ concatMap (bcc f (i+1)) bc ++ indent (i + 1) ++ "break;\n"+    showDef i Nothing = indent i ++ "default:\n" +++                        indent (i + 1) ++ "return NULL;\n"     showDef i (Just c) = indent i ++ "default:\n"-                         ++ concatMap (bcc (i+1)) c ++ indent (i + 1) ++ "break;\n"-bcc i (CONSTCASE r code def)+                         ++ concatMap (bcc f (i+1)) c ++ indent (i + 1) ++ "break;\n"+bcc f i (CONSTCASE r code def)    | intConsts code --      = indent i ++ "switch(GETINT(" ++ creg r ++ ")) {\n" ++ --        concatMap (showCase i) code ++@@ -290,65 +287,67 @@      strCase sv (s, bc) =         indent i ++ "if (strcmp(" ++ sv ++ ", " ++ show s ++ ") == 0) {\n" ++-           concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"+           concatMap (bcc f (i+1)) bc ++ indent i ++ "} else\n"     biCase bv (BI b, bc) =         indent i ++ "if (bigEqConst(" ++ bv ++ ", " ++ show b ++ ")) {\n"-           ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"+           ++ concatMap (bcc f (i+1)) bc ++ indent i ++ "} else\n"     iCase v (I b, bc) =         indent i ++ "if (GETINT(" ++ v ++ ") == " ++ show b ++ ") {\n"-           ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"+           ++ concatMap (bcc f (i+1)) bc ++ indent i ++ "} else\n"     iCase v (Ch b, bc) =         indent i ++ "if (GETINT(" ++ v ++ ") == " ++ show (fromEnum b) ++ ") {\n"-           ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"+           ++ concatMap (bcc f (i+1)) bc ++ indent i ++ "} else\n"     iCase v (B8 w, bc) =         indent i ++ "if (GETBITS8(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"-           ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"+           ++ concatMap (bcc f (i+1)) bc ++ indent i ++ "} else\n"     iCase v (B16 w, bc) =         indent i ++ "if (GETBITS16(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"-           ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"+           ++ concatMap (bcc f (i+1)) bc ++ indent i ++ "} else\n"     iCase v (B32 w, bc) =         indent i ++ "if (GETBITS32(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"-           ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"+           ++ concatMap (bcc f (i+1)) bc ++ indent i ++ "} else\n"     iCase v (B64 w, bc) =         indent i ++ "if (GETBITS64(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"-           ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"+           ++ concatMap (bcc f (i+1)) bc ++ indent i ++ "} else\n"     showDefS i Nothing = ""-    showDefS i (Just c) = concatMap (bcc (i+1)) c+    showDefS i (Just c) = concatMap (bcc f (i+1)) c -bcc i (CALL n) = indent i ++ "CALL(" ++ cname n ++ ");\n"-bcc i (TAILCALL n) = indent i ++ "TAILCALL(" ++ cname n ++ ");\n"-bcc i (SLIDE n) = indent i ++ "SLIDE(vm, " ++ show n ++ ");\n"-bcc i REBASE = indent i ++ "REBASE;\n"-bcc i (RESERVE 0) = ""-bcc i (RESERVE n) = indent i ++ "RESERVE(" ++ show n ++ ");\n"-bcc i (ADDTOP 0) = ""-bcc i (ADDTOP n) = indent i ++ "ADDTOP(" ++ show n ++ ");\n"-bcc i (TOPBASE n) = indent i ++ "TOPBASE(" ++ show n ++ ");\n"-bcc i (BASETOP n) = indent i ++ "BASETOP(" ++ show n ++ ");\n"-bcc i STOREOLD = indent i ++ "STOREOLD;\n"-bcc i (OP l fn args) = indent i ++ doOp (creg l ++ " = ") fn args ++ ";\n"-bcc i (FOREIGNCALL l rty (FStr ('#':name)) [])+bcc f i (CALL n) = indent i ++ "CALL(" ++ cname n ++ ");\n"+bcc f i (TAILCALL n)+    | f == n = indent i ++ "goto loop;\n"+    | otherwise = indent i ++ "TAILCALL(" ++ cname n ++ ");\n"+bcc f i (SLIDE n) = indent i ++ "SLIDE(vm, " ++ show n ++ ");\n"+bcc f i REBASE = indent i ++ "REBASE;\n"+bcc f i (RESERVE 0) = ""+bcc f i (RESERVE n) = indent i ++ "RESERVE(" ++ show n ++ ");\n"+bcc f i (ADDTOP 0) = ""+bcc f i (ADDTOP n) = indent i ++ "ADDTOP(" ++ show n ++ ");\n"+bcc f i (TOPBASE n) = indent i ++ "TOPBASE(" ++ show n ++ ");\n"+bcc f i (BASETOP n) = indent i ++ "BASETOP(" ++ show n ++ ");\n"+bcc f i STOREOLD = indent i ++ "STOREOLD;\n"+bcc f i (OP l fn args) = indent i ++ doOp (creg l ++ " = ") fn args ++ ";\n"+bcc f i (FOREIGNCALL l rty (FStr ('#':name)) [])       = indent i ++         c_irts (toFType rty) (creg l ++ " = ") name ++ ";\n"-bcc i (FOREIGNCALL l rty (FStr fn@('&':name)) [])+bcc f i (FOREIGNCALL l rty (FStr fn@('&':name)) [])       = indent i ++         c_irts (toFType rty) (creg l ++ " = ") fn ++ ";\n"-bcc i (FOREIGNCALL l rty (FStr fn) (x:xs)) | fn == "%wrapper"+bcc f i (FOREIGNCALL l rty (FStr fn) (x:xs)) | fn == "%wrapper"       = indent i ++         c_irts (toFType rty) (creg l ++ " = ")             ("_idris_get_wrapper(" ++ creg (snd x) ++ ")") ++ ";\n"-bcc i (FOREIGNCALL l rty (FStr fn) (x:xs)) | fn == "%dynamic"+bcc f i (FOREIGNCALL l rty (FStr fn) (x:xs)) | fn == "%dynamic"       = indent i ++ c_irts (toFType rty) (creg l ++ " = ")             ("(*(" ++ cFnSig "" rty xs ++ ") GETPTR(" ++ creg (snd x) ++ "))" ++              "(" ++ showSep "," (map fcall xs) ++ ")") ++ ";\n"-bcc i (FOREIGNCALL l rty (FStr fn) args)+bcc f i (FOREIGNCALL l rty (FStr fn) args)       = indent i ++         c_irts (toFType rty) (creg l ++ " = ")                    (fn ++ "(" ++ showSep "," (map fcall args) ++ ")") ++ ";\n"-bcc i (FOREIGNCALL l rty _ args) = error "Foreign Function calls cannot be partially applied, without being inlined."-bcc i (NULL r) = indent i ++ creg r ++ " = NULL;\n" -- clear, so it'll be GCed-bcc i (ERROR str) = indent i ++ "fprintf(stderr, " ++ show str ++ "); fprintf(stderr, \"\\n\"); exit(-1);\n"--- bcc i c = error (show c) -- indent i ++ "// not done yet\n"+bcc f i (FOREIGNCALL l rty _ args) = error "Foreign Function calls cannot be partially applied, without being inlined."+bcc f i (NULL r) = indent i ++ creg r ++ " = NULL;\n" -- clear, so it'll be GCed+bcc f i (ERROR str) = indent i ++ "fprintf(stderr, " ++ show str ++ "); fprintf(stderr, \"\\n\"); exit(-1);\n"+-- bcc f i c = error (show c) -- indent i ++ "// not done yet\n"  fcall (t, arg) = irts_c (toFType t) (creg arg) -- Deconstruct the Foreign type in the defunctionalised expression and build@@ -390,7 +389,7 @@ c_irts FString l x = l ++ "MKSTR(vm, " ++ x ++ ")" c_irts FUnit l x = x c_irts FPtr l x = l ++ "MKPTR(vm, " ++ x ++ ")"-c_irts FManagedPtr l x = l ++ "MKMPTR(vm, " ++ x ++ ")"+c_irts FManagedPtr l x = l ++ x c_irts (FArith ATFloat) l x = l ++ "MKFLOAT(vm, " ++ x ++ ")" c_irts FCData l x = l ++ "MKCDATA(vm, " ++ x ++ ")" c_irts FAny l x = l ++ x@@ -425,6 +424,13 @@ signedTy :: NativeTy -> String signedTy t = "int" ++ show (nativeTyWidth t) ++ "_t" +-- Need to ensure we have enough spare *before* GMP operations because they+-- use the idris allocator but outside our control, and if it GCs in the middle+-- then things get moved which leads to trouble...+-- I'm just guessing how much it'll need. This is a TMP HACK. Sorry.+wrapGMP op+   = "idris_requireAlloc(vm, 65536); " ++ op ++ "; idris_doneAlloc(vm)"+ doOp v (LPlus (ATInt ITNative)) [l, r] = v ++ "ADD(" ++ creg l ++ ", " ++ creg r ++ ")" doOp v (LMinus (ATInt ITNative)) [l, r] = v ++ "INTOP(-," ++ creg l ++ ", " ++ creg r ++ ")" doOp v (LTimes (ATInt ITNative)) [l, r] = v ++ "MULT(" ++ creg l ++ ", " ++ creg r ++ ")"@@ -485,21 +491,21 @@  doOp v (LIntFloat ITBig) [x] = v ++ "idris_castBigFloat(vm, " ++ creg x ++ ")" doOp v (LFloatInt ITBig) [x] = v ++ "idris_castFloatBig(vm, " ++ creg x ++ ")"-doOp v (LPlus (ATInt ITBig)) [l, r] = v ++ "idris_bigPlus(vm, " ++ creg l ++ ", " ++ creg r ++ ")"-doOp v (LMinus (ATInt ITBig)) [l, r] = v ++ "idris_bigMinus(vm, " ++ creg l ++ ", " ++ creg r ++ ")"-doOp v (LTimes (ATInt ITBig)) [l, r] = v ++ "idris_bigTimes(vm, " ++ creg l ++ ", " ++ creg r ++ ")"-doOp v (LSDiv (ATInt ITBig)) [l, r] = v ++ "idris_bigDivide(vm, " ++ creg l ++ ", " ++ creg r ++ ")"-doOp v (LSRem (ATInt ITBig)) [l, r] = v ++ "idris_bigMod(vm, " ++ creg l ++ ", " ++ creg r ++ ")"-doOp v (LAnd ITBig) [l, r] = v ++ "idris_bigAnd(vm, " ++ creg l ++ ", " ++ creg r ++ ")"-doOp v (LOr ITBig) [l, r] = v ++ "idris_bigOr(vm, " ++ creg l ++ ", " ++ creg r ++ ")"-doOp v (LSHL ITBig) [l, r] = v ++ "idris_bigShiftLeft(vm, " ++ creg l ++ ", " ++ creg r ++ ")"-doOp v (LLSHR ITBig) [l, r] = v ++ "idris_bigLShiftRight(vm, " ++ creg l ++ ", " ++ creg r ++ ")"-doOp v (LASHR ITBig) [l, r] = v ++ "idris_bigAShiftRight(vm, " ++ creg l ++ ", " ++ creg r ++ ")"-doOp v (LEq (ATInt ITBig)) [l, r] = v ++ "idris_bigEq(vm, " ++ creg l ++ ", " ++ creg r ++ ")"-doOp v (LSLt (ATInt ITBig)) [l, r] = v ++ "idris_bigLt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"-doOp v (LSLe (ATInt ITBig)) [l, r] = v ++ "idris_bigLe(vm, " ++ creg l ++ ", " ++ creg r ++ ")"-doOp v (LSGt (ATInt ITBig)) [l, r] = v ++ "idris_bigGt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"-doOp v (LSGe (ATInt ITBig)) [l, r] = v ++ "idris_bigGe(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v (LPlus (ATInt ITBig)) [l, r] = wrapGMP $ v ++ "idris_bigPlus(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v (LMinus (ATInt ITBig)) [l, r] = wrapGMP $ v ++ "idris_bigMinus(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v (LTimes (ATInt ITBig)) [l, r] = wrapGMP $ v ++ "idris_bigTimes(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v (LSDiv (ATInt ITBig)) [l, r] = wrapGMP $ v ++ "idris_bigDivide(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v (LSRem (ATInt ITBig)) [l, r] = wrapGMP $ v ++ "idris_bigMod(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v (LAnd ITBig) [l, r] = wrapGMP $ v ++ "idris_bigAnd(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v (LOr ITBig) [l, r] = wrapGMP $ v ++ "idris_bigOr(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v (LSHL ITBig) [l, r] = wrapGMP $ v ++ "idris_bigShiftLeft(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v (LLSHR ITBig) [l, r] = wrapGMP $ v ++ "idris_bigLShiftRight(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v (LASHR ITBig) [l, r] = wrapGMP $ v ++ "idris_bigAShiftRight(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v (LEq (ATInt ITBig)) [l, r] = wrapGMP $ v ++ "idris_bigEq(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v (LSLt (ATInt ITBig)) [l, r] = wrapGMP $ v ++ "idris_bigLt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v (LSLe (ATInt ITBig)) [l, r] = wrapGMP $ v ++ "idris_bigLe(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v (LSGt (ATInt ITBig)) [l, r] = wrapGMP $ v ++ "idris_bigGt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v (LSGe (ATInt ITBig)) [l, r] = wrapGMP $ v ++ "idris_bigGe(vm, " ++ creg l ++ ", " ++ creg r ++ ")"  doOp v (LIntFloat ITNative) [x] = v ++ "idris_castIntFloat(" ++ creg x ++ ")" doOp v (LFloatInt ITNative) [x] = v ++ "idris_castFloatInt(" ++ creg x ++ ")"@@ -645,6 +651,7 @@  doOp v (LExternal vm) [_] | vm == sUN "prim__vm" = v ++ "MKPTR(vm, vm)" doOp v (LExternal nul) [] | nul == sUN "prim__null" = v ++ "MKPTR(vm, NULL)"+doOp v (LExternal nul) [] | nul == sUN "prim__managedNull" = v ++ "MKPTR(vm, NULL)" doOp v (LExternal eqp) [x, y] | eqp == sUN "prim__eqPtr"     = v ++ "MKINT((i_int)(GETPTR(" ++ creg x ++ ") == GETPTR(" ++ creg y ++ ")))" doOp v (LExternal eqp) [x, y] | eqp == sUN "prim__eqManagedPtr"@@ -890,7 +897,10 @@         getCallback' [] = []         findCons (c:cs) xs = findCon c xs ++ findCons cs xs         findCons [] _ = []-        findCon c ((MKCON l loc tag args):xs) | snd c == l = [(fst c, tag)]+        findCon c ((MKCON l loc tag args):xs) | snd c == l =+            if null args+                then [(fst c, tag)]+                else error "Can't wrap a closure as callback."         findCon c (_:xs) = findCon c xs         findCon c [] = [] 

@@ -103,10 +103,10 @@   , item (LSHL (ITFixed IT64)) True PTAny $     \[l, r] -> JsForeign "%0.shiftLeft(%1).and(new $JSRTS.jsbn.BigInteger(%2))" [l,r, JsStr $ show 0xFFFFFFFFFFFFFFFF]   , item (LSHL ITBig) True PTAny $ method "shiftLeft"-  , item (LLSHR ITNative) False PTAny $ JsForeign "%0 >> %1 |0"-  , item (LLSHR (ITFixed IT8)) False PTAny $ JsForeign "%0 >> %1"-  , item (LLSHR (ITFixed IT16)) False PTAny $ JsForeign "%0 >> %1"-  , item (LLSHR (ITFixed IT32)) False PTAny $ JsForeign "%0 >> %1|0"+  , item (LLSHR ITNative) False PTAny $ JsForeign "%0 >>> %1 |0"+  , item (LLSHR (ITFixed IT8)) False PTAny $ JsForeign "%0 >>> %1"+  , item (LLSHR (ITFixed IT16)) False PTAny $ JsForeign "%0 >>> %1"+  , item (LLSHR (ITFixed IT32)) False PTAny $ JsForeign "%0 >>> %1|0"   , item (LLSHR (ITFixed IT64)) True PTAny $ JsForeign "%0.shiftRight(%1)"   , item (LASHR ITNative) False PTAny $ JsForeign "%0 >> %1 |0"   , item (LASHR (ITFixed IT8)) False PTAny $ JsForeign "%0 >> %1"

@@ -455,3 +455,28 @@       showAlt env ind (LConstCase c e) = show c ++ " => " ++ show' env ind e      showAlt env ind (LDefaultCase e) = "_ => " ++ show' env ind e++occName :: Name -> LExp -> Int+occName n (LV x) = if n == x then 1 else 0+occName n (LApp t e es) = occName n e + sum (map (occName n) es)+occName n (LLazyApp x es)+    = if n == x then 1 + sum (map (occName n) es)+                else sum (map (occName n) es)+occName n (LForce e) = occName n e+occName n (LLet x v sc)+    = if n == x then occName n v+                else occName n v + occName n sc+occName n (LLam ns sc)+    = if n `elem` ns then 0 else occName n sc+occName n (LProj e i) = occName n e+occName n (LCon _ _ _ es) = sum (map (occName n) es)+occName n (LCase t e alts) = occName n e + maximum (map occAlt alts)+  where+    occAlt (LConCase _ _ ns e)+        = if n `elem` ns then 0 else occName n e+    occAlt (LConstCase _ e) = occName n e+    occAlt (LDefaultCase e) = occName n e+occName n (LForeign _ _ es) = sum (map (occName n . snd) es)+occName n (LOp _ es) = sum (map (occName n) es)+occName n _ = 0+

@@ -33,16 +33,23 @@ -- uniqueness of variable names in the resulting definition, so invent -- a new name for every variable we encounter doInline :: LDefs -> LDecl -> LDecl-doInline defs d@(LConstructor _ _ _) = d-doInline defs (LFun opts topn args exp)+doInline = doInline' 1++doInline' :: Int -> LDefs -> LDecl -> LDecl+doInline' 0 defs d = d+doInline' i defs d@(LConstructor _ _ _) = d+doInline' i defs (LFun opts topn args exp)       = let inl = evalState (eval [] initEnv [topn] defs exp)                              (length args)             -- do some case floating, which might arise as a result             -- then, eta contract             res = eta $ caseFloats 10 inl in             case res of-                 LLam args' body -> LFun opts topn (map snd initNames ++ args') body-                 _ -> LFun opts topn (map snd initNames) res+                 LLam args' body ->+                   doInline' (i - 1) defs $+                     LFun opts topn (map snd initNames ++ args') body+                 _ -> doInline' (i - 1) defs $+                        LFun opts topn (map snd initNames) res   where     caseFloats 0 tm = tm     caseFloats n tm@@ -72,8 +79,8 @@ eval stk env rec defs (LForce e)     = do e' <- eval [] env rec defs e          case e' of-              LLazyExp forced -> return $ unload stk forced-              LLazyApp n es -> return $ unload stk (LApp False (LV n) es)+              LLazyExp forced -> eval stk env rec defs forced+              LLazyApp n es -> eval stk env rec defs (LApp False (LV n) es)               _ -> return (unload stk (LForce e')) eval stk env rec defs (LLazyExp e)     = unload stk <$> LLazyExp <$> eval [] env rec defs e@@ -92,6 +99,7 @@     = do act' <- eval [] env rec defs (LApp False act [world])          argn <- nextN          k' <- eval stk ((arg, LV argn) : env) rec defs (LApp False k [world])+         -- Needs to be a LLet to make sure the action gets evaluated          return $ LLet argn act' k'  eval stk env rec defs (LApp t f es)@@ -105,16 +113,30 @@     = unload stk <$> (LProj <$> eval [] env rec defs exp <*> return i) eval stk env rec defs (LCon loc i n es)     = unload stk <$> (LCon loc i n <$> mapM (eval [] env rec defs) es)+eval stk env rec defs (LCase ty e [])+    = pure LNothing eval stk env rec defs (LCase ty e alts)-    = do alts' <- mapM (evalAlt stk env rec defs) alts-         e' <- eval [] env rec defs e-         -- If they're all lambdas, bind the lambda at the top-         let prefix = getLams (map getRHS alts')-         case prefix of-              [] -> return $ conOpt $ LCase ty e' (replaceInAlts e' alts')-              args -> do alts_red <- mapM (dropArgs args) alts'-                         return $ LLam args-                            (conOpt (LCase ty e' (replaceInAlts e' alts_red)))+    = do e' <- eval [] env rec defs e+         case evalAlts e' alts of+              Just (env', tm) -> eval stk env' rec defs tm+              Nothing ->+                do alts' <- mapM (evalAlt stk env rec defs) alts+                   -- If they're all lambdas, bind the lambda at the top+                   let prefix = getLams (map getRHS alts')+                   case prefix of+                        [] -> return $ LCase ty e' (replaceInAlts e' alts')+                        args -> do alts_red <- mapM (dropArgs args) alts'+                                   return $ LLam args+                                      (LCase ty e' (replaceInAlts e' alts_red))+  where+    evalAlts e' [] = Nothing+    evalAlts (LCon _ t n args) (LConCase i n' es rhs : as)+        | n == n' = Just (zip es args ++ env, rhs)+    evalAlts (LConst c) (LConstCase c' rhs : as)+        | c == c' = Just (env, rhs)+    evalAlts (LCon _ _ _ _) (LDefaultCase rhs : as) = Just (env, rhs)+    evalAlts (LConst _) (LDefaultCase rhs : as) = Just (env, rhs)+    evalAlts tm (_ : as) = evalAlts tm as eval stk env rec defs (LOp f es)     = unload stk <$> LOp f <$> mapM (eval [] env rec defs) es eval stk env rec defs (LForeign t s args)@@ -129,9 +151,9 @@                [] -> eval stk' env' rec defs sc                as -> do ns' <- mapM (\n -> do n' <- nextN                                               return (n, n')) args'-                        unload stk' <$> LLam (map snd ns') <$>-                            eval [] (map (\ (n, n') -> (n, LV n')) ns' ++ env')-                                    rec defs sc+                        LLam (map snd ns') <$>+                            eval stk' (map (\ (n, n') -> (n, LV n')) ns' ++ env')+                                 rec defs sc eval stk env rec defs var@(LV n)     = case lookup n env of            Just t@@ -164,19 +186,24 @@     = eval stk env rec defs (LLam args body)  dropArgs :: [Name] -> LAlt -> State Int LAlt-dropArgs as (LConCase i n es (LLam args rhs))-    = do let old = take (length as) args-         rhs' <- eval [] (zipWith (\ o n -> (o, LV n)) old as) [] emptyContext rhs+dropArgs as (LConCase i n es t)+    = do rhs' <- dropArgsTm as t          return (LConCase i n es rhs')-dropArgs as (LConstCase c (LLam args rhs))-    = do let old = take (length as) args-         rhs' <- eval [] (zipWith (\ o n -> (o, LV n)) old as) [] emptyContext rhs+dropArgs as (LConstCase c t)+    = do rhs' <- dropArgsTm as t          return (LConstCase c rhs')-dropArgs as (LDefaultCase (LLam args rhs))-    = do let old = take (length as) args-         rhs' <- eval [] (zipWith (\ o n -> (o, LV n)) old as) [] emptyContext rhs+dropArgs as (LDefaultCase t)+    = do rhs' <- dropArgsTm as t          return (LDefaultCase rhs') +dropArgsTm as (LLam args rhs)+    = do let old = take (length as) args+         eval [] (zipWith (\ o n -> (o, LV n)) old as) [] emptyContext rhs+dropArgsTm as (LLet n val rhs)+    = do rhs' <- dropArgsTm as rhs+         pure (LLet n val rhs')+dropArgsTm as tm = return tm+ caseFloat :: LExp -> LExp caseFloat (LApp tc e es) = LApp tc (caseFloat e) (map caseFloat es) caseFloat (LLazyExp e) = LLazyExp (caseFloat e)@@ -272,12 +299,14 @@  getLams [] = [] getLams (LLam args tm : cs) = getLamPrefix args cs+getLams (LLet n val exp : cs) = getLams (exp : cs) getLams _ = []  getLamPrefix as [] = as getLamPrefix as (LLam args tm : cs)     | length args < length as = getLamPrefix args cs     | otherwise = getLamPrefix as cs+getLamPrefix as (LLet n val exp : cs) = getLamPrefix as (exp : cs) getLamPrefix as (_ : cs) = []  -- eta contract ('\x -> f x' can just be compiled as 'f' when f is local)

@@ -83,7 +83,7 @@ #endif  #ifdef IDRIS_GMP-gmpLib = ["-lgmp"]+gmpLib = ["-lgmp", "-DIDRIS_GMP"] #else gmpLib = [] #endif

@@ -302,8 +302,8 @@    , idris_symbols                :: M.Map Name Name           -- ^ Symbol table (preserves sharing of names)   , idris_exports                :: [Name]                    -- ^ Functions with ExportList-  , idris_highlightedRegions     :: [(FC, OutputAnnotation)]  -- ^ Highlighting information to output-  , idris_parserHighlights       :: [(FC, OutputAnnotation)]  -- ^ Highlighting information from the parser+  , idris_highlightedRegions     :: S.Set (FC', OutputAnnotation)  -- ^ Highlighting information to output+  , idris_parserHighlights       :: S.Set (FC', OutputAnnotation)  -- ^ Highlighting information from the parser   , idris_deprecated             :: Ctxt String               -- ^ Deprecated names and explanation   , idris_inmodule               :: S.Set Name                -- ^ Names defined in current module   , idris_ttstats                :: M.Map Term (Int, Term)@@ -411,7 +411,7 @@                    [] [] [] defaultOpts 6 [] [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []                    [] [] Nothing [] Nothing [] [] Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []                    (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty-                   AutomaticWidth S.empty S.empty [] [] [] M.empty [] [] []+                   AutomaticWidth S.empty S.empty [] [] [] M.empty [] S.empty S.empty                    emptyContext S.empty M.empty emptyContext initialInteractiveOpts  @@ -710,19 +710,19 @@     case_decls        :: [(Name, PDecl)]   , delayed_elab      :: [(Int, Elab' EState ())]   , new_tyDecls       :: [RDeclInstructions]-  , highlighting      :: [(FC, OutputAnnotation)]+  , highlighting      :: S.Set (FC', OutputAnnotation)   , auto_binds        :: [Name]        -- ^  names bound as auto implicits   , implicit_warnings :: [(FC, Name)] -- ^ Implicit warnings to report (location and global name)   }  initEState :: EState-initEState = EState [] [] [] [] [] []+initEState = EState [] [] [] S.empty [] []  type ElabD a = Elab' EState a  highlightSource :: FC -> OutputAnnotation -> ElabD () highlightSource fc annot =-  updateAux (\aux -> aux { highlighting = (fc, annot) : highlighting aux })+  updateAux (\aux -> aux { highlighting = S.insert (FC' fc, annot) (highlighting aux) })  -- | One clause of a top-level definition. Term arguments to constructors are: --

@@ -549,19 +549,19 @@      altGroup n i args          = do inacc <- inaccessibleArgs n-              (newVars, accVars, inaccVars, nextCs) <- argsToAlt inacc args+              ~(newVars, accVars, inaccVars, nextCs) <- argsToAlt inacc args               matchCs <- match (accVars ++ vs ++ inaccVars) nextCs err               return $ ConCase n i newVars matchCs -    altFnGroup n args = do (newVars, _, [], nextCs) <- argsToAlt [] args+    altFnGroup n args = do ~(newVars, _, [], nextCs) <- argsToAlt [] args                            matchCs <- match (newVars ++ vs) nextCs err                            return $ FnCase n newVars matchCs -    altSucGroup args = do ([newVar], _, [], nextCs) <- argsToAlt [] args+    altSucGroup args = do ~([newVar], _, [], nextCs) <- argsToAlt [] args                           matchCs <- match (newVar:vs) nextCs err                           return $ SucCase newVar matchCs -    altConstGroup n args = do (_, _, [], nextCs) <- argsToAlt [] args+    altConstGroup n args = do ~(_, _, [], nextCs) <- argsToAlt [] args                               matchCs <- match vs nextCs err                               return $ ConstCase n matchCs 

@@ -197,10 +197,10 @@     show (FileFC f) = f  -- | Output annotation for pretty-printed name - decides colour-data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput | PostulateOutput deriving (Show, Eq, Generic)+data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput | PostulateOutput deriving (Show, Eq, Ord, Generic)  -- | Text formatting output-data TextFormatting = BoldText | ItalicText | UnderlineText deriving (Show, Eq, Generic)+data TextFormatting = BoldText | ItalicText | UnderlineText deriving (Show, Eq, Ord, Generic)  -- | Output annotations for pretty-printing data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe String)@@ -227,7 +227,7 @@                       | AnnQuasiquote                       | AnnAntiquote                       | AnnSyntax String -- ^ type of syntax element: backslash or braces etc.-  deriving (Show, Eq, Generic)+  deriving (Show, Eq, Generic, Ord)  -- | Used for error reflection data ErrorReportPart = TextPart String

@@ -13,6 +13,8 @@ import Idris.Imports import Idris.Output (sendHighlighting) +import qualified Data.Set as S+ import Util.DynamicLinker  -- | Run the action corresponding to a directive@@ -81,7 +83,7 @@   ty' <- disambiguate ty   mapM_ (addNameHint ty' . fst) ns   mapM_ (\n -> addIBC (IBCNameHint (ty', fst n))) ns-  sendHighlighting $ [(tyFC, AnnName ty' Nothing Nothing Nothing)] ++ map (\(n, fc) -> (fc, AnnBoundName n False)) ns+  sendHighlighting $ S.fromList $ [(FC' tyFC, AnnName ty' Nothing Nothing Nothing)] ++ map (\(n, fc) -> (FC' fc, AnnBoundName n False)) ns  directiveAction (DErrorHandlers fn nfc arg afc ns) = do   fn' <- disambiguate fn@@ -90,10 +92,10 @@                   return (n', fc)) ns   addFunctionErrorHandlers fn' arg (map fst ns')   mapM_ (addIBC . IBCFunctionErrorHandler fn' arg . fst) ns'-  sendHighlighting $-       [ (nfc, AnnName fn' Nothing Nothing Nothing)-       , (afc, AnnBoundName arg False)-       ] ++ map (\(n, fc) -> (fc, AnnName n Nothing Nothing Nothing)) ns'+  sendHighlighting $ S.fromList $+       [ (FC' nfc, AnnName fn' Nothing Nothing Nothing)+       , (FC' afc, AnnBoundName arg False)+       ] ++ map (\(n, fc) -> (FC' fc, AnnName n Nothing Nothing Nothing)) ns'  directiveAction (DLanguage ext) = addLangExt ext 

@@ -44,6 +44,7 @@ import Control.Monad.State.Strict as State import Data.List import Data.Maybe+import qualified Data.Set as S import Data.Word import Debug.Trace import Numeric@@ -719,12 +720,9 @@                                                        [] (constraintNS info) fc id [] lhs_tm                                else return (lhs_tm, lhs_ty)         let clhs = normalise ctxt [] clhs_c-        let borrowed = borrowedNames [] clhs-         -- These are the names we're not allowed to use on the RHS, because         -- they're UniqueTypes and borrowed from another function.-        when (not (null borrowed)) $-          logElab 5 ("Borrowed names on LHS: " ++ show borrowed)+        let borrowed = borrowedNames [] clhs          logElab 3 ("Normalised LHS: " ++ showTmImpls (delabMV i clhs)) @@ -1028,7 +1026,7 @@                        Just (n, nfc) -> Just (uniqueName n (map fst bargs))          -- Highlight explicit proofs-        sendHighlighting [(fc, AnnBoundName n False) | (n, fc) <- maybeToList pn_in]+        sendHighlighting $ S.fromList [(FC' fc, AnnBoundName n False) | (n, fc) <- maybeToList pn_in]          logElab 10 ("With type " ++ show (getRetTy cwvaltyN) ++                   " depends on " ++ show pdeps ++ " from " ++ show pvars)

@@ -37,6 +37,7 @@ import Data.List import qualified Data.Map as Map import Data.Maybe+import qualified Data.Set as S import qualified Data.Text as T  warnLC :: FC -> Name -> Idris ()@@ -53,7 +54,7 @@           addIBC (IBCDef n)          updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons-         sendHighlighting [(nfc, AnnName n Nothing Nothing Nothing)]+         sendHighlighting $ S.fromList [(FC' nfc, AnnName n Nothing Nothing Nothing)]  elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)     = do let codata = Codata `elem` opts@@ -118,9 +119,9 @@          when (n /= sUN "=") $             elabRewriteLemma info n cty          -- Emit highlighting info-         sendHighlighting $ [(nfc, AnnName n Nothing Nothing Nothing)] +++         sendHighlighting $ S.fromList $ [(FC' nfc, AnnName n Nothing Nothing Nothing)] ++            map (\(_, _, n, nfc, _, _, _) ->-                 (nfc, AnnName n Nothing Nothing Nothing))+                 (FC' nfc, AnnName n Nothing Nothing Nothing))                dcons   where         checkDefinedAs fc n t i

@@ -26,6 +26,7 @@ import Data.Generics.Uniplate.Data (transform) import Data.List import Data.Maybe+import qualified Data.Set as S  data MArgTy = IA Name | EA Name | CA deriving Show @@ -167,11 +168,11 @@              mapM_ (rec_elabDecl info EAll info) (concatMap (snd.snd) defs)              addIBC (IBCInterface tn) -             sendHighlighting $-               [(tnfc, AnnName tn Nothing Nothing Nothing)] ++-               [(pnfc, AnnBoundName pn False) | (pn, pnfc, _) <- ps] ++-               [(fdfc, AnnBoundName fc False) | (fc, fdfc) <- fds] ++-               maybe [] (\(conN, conNFC) -> [(conNFC, AnnName conN Nothing Nothing Nothing)]) mcn+             sendHighlighting $ S.fromList $+               [(FC' tnfc, AnnName tn Nothing Nothing Nothing)] +++               [(FC' pnfc, AnnBoundName pn False) | (pn, pnfc, _) <- ps] +++               [(FC' fdfc, AnnBoundName fc False) | (fc, fdfc) <- fds] +++               maybe [] (\(conN, conNFC) -> [(FC' conNFC, AnnName conN Nothing Nothing Nothing)]) mcn    where     info = info_in { noCaseLift = tn : noCaseLift info_in }

@@ -20,6 +20,7 @@ import Control.Monad import Data.List import Data.Maybe+import qualified Data.Set as S  -- | Elaborate a record declaration elabRecord :: ElabInfo@@ -66,10 +67,10 @@            logElab 1 $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc            elabRecordFunctions info rsyn fc tyn paramsAndDoc fieldsWithNameAndDoc dconName target -           sendHighlighting $-             [(nfc, AnnName tyn Nothing Nothing Nothing)] ++-             maybe [] (\(_, cnfc) -> [(cnfc, AnnName dconName Nothing Nothing Nothing)]) cname ++-             [(ffc, AnnBoundName fn False) | (fn, ffc, _, _, _) <- fieldsWithName]+           sendHighlighting $ S.fromList $+             [(FC' nfc, AnnName tyn Nothing Nothing Nothing)] +++             maybe [] (\(_, cnfc) -> [(FC' cnfc, AnnName dconName Nothing Nothing Nothing)]) cname +++             [(FC' ffc, AnnBoundName fn False) | (fn, ffc, _, _, _) <- fieldsWithName]    where     -- | Generates a type constructor.

@@ -56,7 +56,7 @@     -- | Meta-info about the new type declarations   , resultTyDecls :: [RDeclInstructions]     -- | Saved highlights from elaboration-  , resultHighlighting :: [(FC, OutputAnnotation)]+  , resultHighlighting :: S.Set (FC', OutputAnnotation)     -- | The new global name counter   , resultName :: Int   }@@ -448,7 +448,7 @@              -- the full set.              uns <- get_usedns              let as' = map (mkUniqueNames (uns ++ map snd ms) ms) as_pruned-             (h : hs) <- get_holes+             ~(h : hs) <- get_holes              ty <- goal              case as' of                   [] -> do hds <- mapM showHd as@@ -984,7 +984,7 @@                                             (elab' ina fc Placeholder)                                             (show f)     elab' ina fc Placeholder-        = do (h : hs) <- get_holes+        = do ~(h : hs) <- get_holes              movelast h     elab' ina fc (PMetavar nfc n) =           do ptm <- get_term@@ -1251,7 +1251,7 @@     elab' ina fc (PHidden t)       | reflection = elab' ina fc t       | otherwise-        = do (h : hs) <- get_holes+        = do ~(h : hs) <- get_holes              -- Dotting a hole means that either the hole or any outer              -- hole (a hole outside any occurrence of it)              -- must be solvable by unification as well as being filled@@ -1259,7 +1259,7 @@              -- Delay dotted things to the end, then when we elaborate them              -- we can check the result against what was inferred              movelast h-             (h' : hs) <- get_holes+             ~(h' : hs) <- get_holes              -- If we're at the end anyway, do it now              if h == h' then elabHidden h                         else delayElab 10 $ elabHidden h

@@ -205,7 +205,7 @@                  else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler"              else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."          -- Send highlighting information about the name being declared-         sendHighlighting [(nfc, AnnName n Nothing Nothing Nothing)]+         sendHighlighting $ S.fromList [(FC' nfc, AnnName n Nothing Nothing Nothing)]          -- if it's an export list type, make a note of it          case (unApply usety) of               (P _ ut _, _)@@ -238,7 +238,7 @@     elabType info syn doc [] fc opts n NoFC ty     putIState . (\ist -> ist{ idris_postulates = S.insert n (idris_postulates ist) }) =<< getIState     addIBC (IBCPostulate n)-    sendHighlighting [(nfc, AnnName n (Just PostulateOutput) Nothing Nothing)]+    sendHighlighting $ S.fromList [(FC' nfc, AnnName n (Just PostulateOutput) Nothing Nothing)]      -- remove it from the deferred definitions list     solveDeferred fc n

@@ -26,6 +26,7 @@  import Control.Category import Data.Char (toLower)+import qualified Data.Set as S () import qualified Data.Traversable as Traversable  -- | Elaborate a value, returning any new bindings created (this will only

@@ -41,8 +41,10 @@ import Control.Monad import Control.Monad.State.Strict as State import Data.Maybe+import qualified Data.Set as S import qualified Data.Text as T + -- | Top level elaborator info, supporting recursive elaboration recinfo :: FC -> ElabInfo recinfo fc = EInfo [] emptyContext id [] (Just fc) (fc_fname fc) 0 [] id elabDecl'@@ -260,7 +262,7 @@ elabDecl' what info (PNamespace n nfc ps) =   do mapM_ (elabDecl' what ninfo) ps      let ns = reverse (map T.pack newNS)-     sendHighlighting [(nfc, AnnNamespace ns Nothing)]+     sendHighlighting $ S.fromList [(FC' nfc, AnnNamespace ns Nothing)]   where     newNS = n : namespace info     ninfo = info { namespace = newNS }

@@ -572,6 +572,9 @@     getDepsTerm vs bs cd (Proj t (-1)) = getDepsTerm vs bs cd t  -- naturals, (S n) -> n     getDepsTerm vs bs cd (Proj t i) = error $ "cannot[1] analyse projection !" ++ show i ++ " of " ++ show t +    -- inferred term+    getDepsTerm vs bs cd (Inferred t) = getDepsTerm vs bs cd t+     -- the easy cases     getDepsTerm vs bs cd (Constant _) = M.empty     getDepsTerm vs bs cd (TType    _) = M.empty

@@ -403,7 +403,7 @@                             --   documentation will be written.             -> IO () createIndex nss out =-  do (path, h) <- openTempFile out "index.html"+  do (path, h) <- openTempFileWithDefaultPermissions out "index.html"      BS2.hPut h $ renderHtml $ wrapper Nothing $ do        H.h1 "Namespaces"        H.ul ! class_ "names" $ do@@ -427,15 +427,14 @@                         --   documentation will be written.             -> IO () createNsDoc ist ns content out =-  do let tpath                   = out </> "docs" </> (genRelNsPath ns "html")-         dir                     = takeDirectory tpath-         file                    = takeFileName tpath-         haveDocs (_, Just d, _) = [d]-         haveDocs _              = []+  do let tpath               = out </> "docs" </> (genRelNsPath ns "html")+         dir                 = takeDirectory tpath+         file                = takeFileName tpath+         haveDocs (_, md, _) = md                                  -- We cannot do anything without a Doc-         content'                = concatMap haveDocs (nsContents content)+         content'            = reverse $ mapMaybe haveDocs $ nsContents content      createDirectoryIfMissing True dir-     (path, h) <- openTempFile dir file+     (path, h) <- openTempFileWithDefaultPermissions dir file      BS2.hPut h $ renderHtml $ wrapper (Just ns) $ do        H.h1 $ toHtml (nsName2Str ns)        case nsDocstring content of

@@ -112,6 +112,7 @@                                             putIState (i { default_total = DefaultCheckingTotal })        tty <- runIO isATTY        setColourise $ not quiet && last (tty : opt getColour opts)+       runIO $ hSetBuffering stdout LineBuffering   @@ -180,8 +181,6 @@        let efile = case inputs of                         [] -> ""                         (f:_) -> f--       runIO $ hSetBuffering stdout LineBuffering         ok <- noErrors        when ok $ case output of

@@ -40,6 +40,7 @@ import Control.Monad.Trans.Except (ExceptT(ExceptT), runExceptT) import Data.List (intersperse, nub) import Data.Maybe (fromJust, fromMaybe, isJust, listToMaybe)+import qualified Data.Set as S import System.Console.Haskeline.MonadException (MonadException(controlIO),                                                 RunIO(RunIO)) import System.FilePath (replaceExtension)@@ -77,9 +78,12 @@     maybeSource <- case messageSource w of                      Just src -> pure (Just src)                      Nothing  -> readSource fc-    let maybeFormattedSource = maybeSource >>= layoutSource fc (idris_highlightedRegions i)+    let maybeFormattedSource = maybeSource >>= layoutSource fc (regions (idris_highlightedRegions i))     return $ layoutMessage (layoutFC fc) maybeFormattedSource (messageText w)   where+    regions :: S.Set (FC', OutputAnnotation) -> [(FC, OutputAnnotation)]+    regions rs = map (\(FC' a,b) -> (a, b)) $ S.toList rs+     fc :: FC     fc = messageExtent w @@ -359,25 +363,23 @@ sendParserHighlighting :: Idris () sendParserHighlighting =   do ist <- getIState-     let hs = map unwrap . nub . map wrap $ idris_parserHighlights ist+     let hs = idris_parserHighlights ist      sendHighlighting hs      ist <- getIState-     putIState ist {idris_parserHighlights = []}-  where wrap (fc, a) = (FC' fc, a)-        unwrap (fc', a) = (unwrapFC fc', a)+     putIState ist {idris_parserHighlights = S.empty} -sendHighlighting :: [(FC, OutputAnnotation)] -> Idris ()+sendHighlighting :: S.Set (FC', OutputAnnotation) -> Idris () sendHighlighting highlights =   do ist <- getIState      case idris_outputmode ist of        RawOutput _ -> updateIState $                       \ist -> ist { idris_highlightedRegions =-                                      highlights ++ idris_highlightedRegions ist }+                                      S.union highlights (idris_highlightedRegions ist) }        IdeMode n h ->          let fancier = [ toSExp (fc, fancifyAnnots ist False annot)-                       | (fc, annot) <- highlights, fullFC fc-                       ]-         in case fancier of+                       | (FC' fc, annot) <- S.toList highlights, fullFC fc+                       ] in+            case fancier of               [] -> return ()               _  -> runIO . hPutStrLn h $                       convSExp "output"@@ -392,7 +394,7 @@ writeHighlights :: FilePath -> Idris () writeHighlights f =   do ist <- getIState-     let hs = reverse $ idris_highlightedRegions ist+     let hs = reverse $ map (\(FC' a, b) -> (a,b)) $ S.toList (idris_highlightedRegions ist)      let hfile = replaceExtension f "idh"      let annots = toSExp [ (fc, fancifyAnnots ist False annot)                          | (fc@(FC _ _ _), annot) <- hs@@ -400,7 +402,7 @@      runIO $ writeFile hfile $ sExpToString annots  clearHighlights :: Idris ()-clearHighlights = updateIState $ \ist -> ist { idris_highlightedRegions = [] }+clearHighlights = updateIState $ \ist -> ist { idris_highlightedRegions = S.empty }  renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String renderExternal fmt width doc

@@ -53,6 +53,7 @@ import qualified Data.Map as M import Data.Maybe import Data.Ord+import qualified Data.Set as S import qualified Data.Text as T import qualified System.Directory as Dir (makeAbsolute) import System.FilePath@@ -1491,7 +1492,7 @@               Right (x, annots, i) ->                 do putIState i                    fname' <- runIO $ Dir.makeAbsolute fname-                   sendHighlighting $ addPath annots fname'+                   sendHighlighting $ S.fromList $ addPath annots fname'                    return x   where imports :: IdrisParser ((Maybe (Docstring ()), [String],                                  [ImportInfo],@@ -1512,11 +1513,11 @@                      let ps = ps_exp -- imp "Builtins" : imp "Prelude" : ps_exp                      return ((mdoc, mname, ps, mrk'), annots, i) -        addPath :: [(FC, OutputAnnotation)] -> FilePath -> [(FC, OutputAnnotation)]+        addPath :: [(FC, OutputAnnotation)] -> FilePath -> [(FC', OutputAnnotation)]         addPath [] _ = []         addPath ((fc, AnnNamespace ns Nothing) : annots) path =-           (fc, AnnNamespace ns (Just path)) : addPath annots path-        addPath (annot:annots) path = annot : addPath annots path+           (FC' fc, AnnNamespace ns (Just path)) : addPath annots path+        addPath ((fc,annot):annots) path = (FC' fc, annot) : addPath annots path          shebang :: IdrisParser ()         shebang = string "#!" *> many (P.satisfy $ not . isEol) *> eol *> pure ()@@ -1664,7 +1665,7 @@                                            srcFnAbs <- case srcFn of                                                          Just fn -> fmap Just (runIO $ Dir.makeAbsolute fn)                                                          Nothing -> return Nothing-                                           sendHighlighting [(nfc, AnnNamespace ns srcFnAbs)])+                                           sendHighlighting $ S.fromList [(FC' nfc, AnnNamespace ns srcFnAbs)])                         [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports]                   reportParserWarnings                   sendParserHighlighting

@@ -89,6 +89,7 @@ import qualified Data.List.NonEmpty as NonEmpty import qualified Data.Map as M import Data.Maybe+import qualified Data.Set as S import qualified Data.Text as T import Text.Megaparsec ((<?>)) import qualified Text.Megaparsec as P@@ -112,7 +113,7 @@ highlight :: (MonadState IState m, Parsing m) => OutputAnnotation -> m a -> m a highlight annot p = do   (result, fc) <- withExtent p-  modify $ \ist -> ist { idris_parserHighlights = (fc, annot) : idris_parserHighlights ist }+  modify $ \ist -> ist { idris_parserHighlights = S.insert (FC' fc, annot) (idris_parserHighlights ist) }   return result  -- | Parse a reserved identfier, highlighting it as a keyword

@@ -30,13 +30,22 @@ -- using pre-build and user-defined operator/fixity declarations table :: [FixDecl] -> [[P.Operator IdrisParser PTerm]] table fixes-   = [[prefix "-" (\fc x -> PApp fc (PRef fc [fc] (sUN "negate")) [pexp x])]] +++   = [[prefix "-" negateExpr]] ++       toTable (reverse fixes) ++      [[noFixityBacktickOperator],       [binary "$" P.InfixR $ \fc _ x y -> flatten $ PApp fc x [pexp y]],       [binary "=" P.InfixL $ \fc _ x y -> PApp fc (PRef fc [fc] eqTy) [pexp x, pexp y]],       [noFixityOperator]]   where++    negateExpr                               :: FC -> PTerm -> PTerm+    negateExpr _  (PConstant fc (I int))     = PConstant fc $ I $ negate int+    negateExpr _  (PConstant fc (BI bigInt)) = PConstant fc $ BI $ negate bigInt+    negateExpr _  (PConstant fc (Fl dbl))    = PConstant fc $ Fl $ negate dbl+    negateExpr _  (PConstSugar fc term)      = negateExpr fc term+    negateExpr fc (PAlternative ns tp terms) = PAlternative ns tp $ map (negateExpr fc) terms+    negateExpr fc x                          = PApp fc (PRef fc [fc] (sUN "negate")) [pexp x]+     flatten                            :: PTerm -> PTerm -- flatten application     flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))     flatten t                          = t

@@ -117,9 +117,9 @@ -- extent is taking trailing whitespace, it's likely there's a double-wrapped -- parser (usually via @Idris.Parser.Helpers.token@). trackExtent :: Parsing m => m a -> m a-trackExtent p = do (FC f (sr, sc) _) <- getFC+trackExtent p = do ~(FC f (sr, sc) _) <- getFC                    result <- p-                   (FC f _ (er, ec)) <- getFC+                   ~(FC f _ (er, ec)) <- getFC                    addExtent (FC f (sr, sc) (er, max 1 (ec - 1)))                    return result 

@@ -416,9 +416,13 @@ getInt _ = []  strToInt :: IntTy -> [Const] -> Maybe Const-strToInt ity [Str x] = case reads x of+strToInt ity [Str x] = case reads $ dropFirstPlus x of                          [(n,s)] -> Just $ if all isSpace s then toInt ity (n :: Integer) else I 0                          _       -> Just $ I 0+  where+    dropFirstPlus :: String -> String+    dropFirstPlus ('+' : str) = str+    dropFirstPlus str = str strToInt _ _ = Nothing  intToFloat :: [Const] -> Maybe Const

@@ -81,7 +81,7 @@ import Idris.WhoCalls import IRTS.CodegenCommon import IRTS.Compiler-import Network+import Network.Socket hiding (defaultPort) #if (MIN_VERSION_base(4,11,0)) import Prelude hiding (id, (.), (<$>), (<>)) #else@@ -166,7 +166,8 @@         fn = fromMaybe "" (listToMaybe fn_in)          loop fn ist sock-            = do (h,_,_) <- accept sock+            = do (s, _) <- accept sock+                 h <- socketToHandle s ReadWriteMode                  hSetEncoding h utf8                  cmd <- hGetLine h                  let isth = case idris_outputmode ist of@@ -218,9 +219,11 @@ runClient :: Maybe PortNumber -> String -> IO () runClient port str = withSocketsDo $ do               let port' = fromMaybe defaultPort port-              res <- X.try (connectTo "localhost" $ PortNumber port')+              s <- socket AF_INET Stream defaultProtocol+              res <- X.try (connect s (SockAddrInet port' $ tupleToHostAddress (127,0,0,1)))               case res of-                Right h -> do+                Right () -> do+                  h <- socketToHandle s ReadWriteMode                   hSetEncoding h utf8                   hPutStrLn h str                   resp <- hGetResp "" h@@ -245,7 +248,8 @@ initIdemodeSocket = do   (sock, port) <- listenOnLocalhostAnyPort   putStrLn $ show port-  (h, _, _) <- accept sock+  (s, _) <- accept sock+  h <- socketToHandle s ReadWriteMode   hSetEncoding h utf8   return h @@ -1229,8 +1233,8 @@           let metavars = mapMaybe (\n -> do c <- lookup n (idris_metavars ist); return (n, c)) ns           n <- case metavars of               [] -> ierror (Msg $ "Cannot find metavariable " ++ show n')-              [(n, (_,_,_,False,_))] -> return n-              [(_, (_,_,_,_,False))]  -> ierror (Msg "Can't prove this hole as it depends on other holes")+              [(n, (_,_,_,False,_))] -> return n+              [(_, (_,_,_,_,False))] -> ierror (Msg "Can't prove this hole as it depends on other holes")               [(_, (_,_,_,True,_))]  -> ierror (Msg "Declarations not solvable using prover")               ns -> ierror (CantResolveAlts (map fst ns))           prover (toplevelWith fn) mode (lit fn) n

@@ -8,36 +8,33 @@ module Util.Net (listenOnLocalhost, listenOnLocalhostAnyPort) where  import Control.Exception (bracketOnError)-import Network hiding (socketPort)-import Network.BSD (getProtocolNumber)-import Network.Socket hiding (sClose)-+import Network.Socket -- Copied from upstream impl of listenOn -- bound to localhost interface instead of iNADDR_ANY listenOnLocalhost :: PortNumber -> IO Socket listenOnLocalhost port = do-    proto <- getProtocolNumber "tcp"-    localhost <- inet_addr "127.0.0.1"+    let hints = defaultHints { addrSocketType = Stream }+    localhost:_ <- getAddrInfo (Just hints) (Just "127.0.0.1") (Just $ show port)     bracketOnError-      (socket AF_INET Stream proto)+      (socket AF_INET Stream defaultProtocol)       (close)       (\sock -> do           setSocketOption sock ReuseAddr 1-          bind sock (SockAddrInet port localhost)+          bind sock (addrAddress localhost)           listen sock maxListenQueue           return sock       )  listenOnLocalhostAnyPort :: IO (Socket, PortNumber) listenOnLocalhostAnyPort = do-    proto <- getProtocolNumber "tcp"-    localhost <- inet_addr "127.0.0.1"+    let hints = defaultHints { addrSocketType = Stream }+    localhost:_ <- getAddrInfo (Just hints) (Just "127.0.0.1") (Just "0")     bracketOnError-      (socket AF_INET Stream proto)+      (socket AF_INET Stream defaultProtocol)       (close)       (\sock -> do           setSocketOption sock ReuseAddr 1-          bind sock (SockAddrInet aNY_PORT localhost)+          bind sock (addrAddress localhost)           listen sock maxListenQueue           port <- socketPort sock           return (sock, port)

@@ -3,10 +3,12 @@  let   libs = [+    gmp     libffi-    zlib     ncurses-    gmp+    nodejs+    perl+    zlib   ];   native_libs = lib.optionals stdenv.isDarwin (with darwin.apple_sdk.frameworks; [     Cocoa

@@ -1,5 +1,5 @@ #recheck extra-deps next on resolver or cabal file change-resolver: lts-11.3+resolver: lts-11.14  packages:   - location: .

@@ -19,11 +19,6 @@ Unique1 : (t0 -> Type) -> Type Unique1 {t0} t1 = (v : t0) -> Unique0 (t1 v) -namespace Iso--  from : {A, B : Type} -> Iso A B -> (B -> A)-  from (MkIso to from toFrom fromTo) = from- namespace Fin    ||| 'Tail' of a finite function

@@ -2,9 +2,9 @@ Type checking ./NumOps.idr Type checking ./Test.idr Leaving directory `./src'+Entering directory `./src' Test Passed Test Passed-Entering directory `./src' Leaving directory `./src' Entering directory `./src' Removed: NumOps.ibc

@@ -0,0 +1,69 @@+{-+See: http://lpaste.net/104020+  and https://github.com/gonzaw/extensible-records+-}+module Record++import Data.List++%default total++data HList : List Type -> Type where+  Nil : HList []+  (::) : a -> HList xs -> HList (a :: xs)++infix 5 :=++data Field : lbl -> Type -> Type where+  (:=) : (label : lbl) ->+          (value : b) -> Field label b++labelsOf : List (lbl, Type) -> List lbl+labelsOf [] = []+labelsOf ((label, _) :: xs) = label :: labelsOf xs++toFields : List (lbl, Type) -> List Type+toFields [] = []+toFields ((l, t) :: xs) = (Field l t) :: toFields xs++data IsSet : List t -> Type where+  IsSetNil : IsSet []+  IsSetCons : Not (Elem x xs) -> IsSet xs -> IsSet (x :: xs)++data Record : List (lty, Type) -> Type where+  MkRecord : IsSet (labelsOf ts) -> HList (toFields ts) ->+                                    Record ts++infixr 6 +:++rnil : Record []+rnil = MkRecord IsSetNil []++prepend : { label : lbl,+          xs : List (lbl, Type),+          prf : Not (Elem label (labelsOf xs))+        } ->+        Field label t ->+        Record xs ->+        Record ((label, t) :: xs)+prepend {prf} f (MkRecord isSet fs) = MkRecord (IsSetCons prf isSet) (f :: fs)++data IsNo : Dec prop -> Type where+  ItIsNo : IsNo (No yprf)++(+:) : DecEq lbl =>+  { label : lbl, xs : List (lbl, Type) } ->+  Field label t ->+  Record xs ->+  { auto isno : IsNo (isElem label $ labelsOf xs) } ->+  Record ((label, t) :: xs)++(+:) {label} {xs} f r with (isElem label $ labelsOf xs)+    (+:) { isno = ItIsNo } _ _ | (Yes _) impossible+    (+:) f r | (No no) = prepend {prf = no} f r++foo : Record [("Year", Integer)]++bar : Record [("Title", String), ("Year", Integer)]+bar = (+:) ("Title" := "test") foo+

@@ -1,7 +1,7 @@ #!/usr/bin/env bash ${IDRIS:-idris} $@ --check \     reg001.idr reg002.idr reg003.idr reg004.lidr reg005.idr \-    reg006.idr reg036.idr reg037.idr reg038.idr reg046.idr \+    reg006.idr reg007.idr reg036.idr reg037.idr reg038.idr reg046.idr \     reg047a.idr reg053.idr reg057.idr reg058.idr reg058a.idr \     reg059.idr reg060.idr  reg061.idr reg062.idr reg063.idr \     reg064.idr reg065.idr  reg066.idr reg071.idr reg074.idr \

@@ -0,0 +1,2 @@+f : Int -> Int+f (-1) = 1

@@ -346,7 +346,7 @@         Type mismatch between                 x = x (Type of Refl)         and-                (-0.0) = 0.0 (Expected type)+                -0.0 = 0.0 (Expected type)                  Specifically:                 Type mismatch between

@@ -35,6 +35,7 @@ :load reg077.idr :load DoubleEquality.idr :load Canonicity.idr+:load Negation.idr !  rm -f *.ibc