idris 0.99 → 0.99.1

raw patch · 220 files changed

+4851/−2248 lines, 220 filesdep +code-pagedep +minttydep +tagsoupdep ~blaze-htmldep ~blaze-markupdep ~safePVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: code-page, mintty, tagsoup

Dependency ranges changed: blaze-html, blaze-markup, safe

API changes (from Hackage documentation)

Files

• .stylish-haskell.yaml +154/−0
• .travis.yml +11/−1
• CHANGELOG.md +52/−0
• CONTRIBUTORS +3/−0
• HLint.hs +1/−0
• INSTALL.md +16/−6
• Makefile +5/−2
• RELEASE-CHECKS.md +1/−0
• config.mk +3/−1
• docs/conf.py +4/−4
• docs/listing/idris-prompt-helloworld.txt +1/−1
• docs/listing/idris-prompt-interp.txt +1/−1
• docs/listing/idris-prompt-start.txt +1/−1
• docs/reference/compilation.rst +23/−7
• docs/reference/documenting.rst +8/−1
• docs/reference/ffi.rst +1/−1
• docs/reference/misc.rst +1/−1
• docs/reference/packages.rst +10/−1
• docs/reference/syntax-guide.rst +70/−0
• docs/tutorial/index.rst +0/−1
• docs/tutorial/interfaces.rst +10/−0
• docs/tutorial/modules.rst +22/−0
• docs/tutorial/packages.rst +101/−15
• docs/tutorial/syntax.rst +1/−1
• docs/tutorial/testing.rst +0/−85
• docs/tutorial/theorems.rst +1/−1
• docs/tutorial/typesfuns.rst +1/−1
• idris.cabal +17/−5
• libs/base/Control/Isomorphism.idr +5/−0
• libs/base/Data/Bits.idr +54/−4
• libs/base/Data/Complex.idr +11/−3
• libs/base/Data/List/Views.idr +0/−2
• libs/base/Data/String/Views.idr +2/−0
• libs/base/Debug/Error.idr +3/−6
• libs/base/Language/Reflection/Utils.idr +12/−0
• libs/base/System.idr +37/−5
• libs/base/base.ipkg +1/−1
• libs/contrib/CFFI/Types.idr +3/−1
• libs/contrib/Control/ST.idr +541/−0
• libs/contrib/Control/ST/ImplicitCall.idr +13/−0
• libs/contrib/Data/List/Zipper.idr +160/−0
• libs/contrib/Data/Monoid.idr +33/−0
• libs/contrib/Data/ZZ.idr +201/−5
• libs/contrib/Interfaces/Verified.idr +1/−1
• libs/contrib/Network/Socket.idr +15/−396
• libs/contrib/Network/Socket/Data.idr +172/−0
• libs/contrib/Network/Socket/Raw.idr +202/−0
• libs/contrib/contrib.ipkg +4/−2
• libs/effects/Effect/Exception.idr +1/−2
• libs/effects/effects.ipkg +1/−1
• libs/prelude/Builtins.idr +7/−0
• libs/prelude/Prelude.idr +11/−3
• libs/prelude/Prelude/Chars.idr +7/−2
• libs/prelude/Prelude/List.idr +9/−4
• libs/prelude/Prelude/Nat.idr +13/−8
• libs/prelude/Prelude/Strings.idr +19/−14
• libs/prelude/prelude.ipkg +1/−1
• libs/pruviloj/Pruviloj/Induction.idr +3/−1
• libs/pruviloj/pruviloj.ipkg +1/−1
• main/Main.hs +7/−7
• man/idris.1 +5/−4
• mkpkg.sh +4/−1
• rts/idris_bitstring.c +8/−8
• rts/idris_gc.c +2/−1
• rts/idris_gmp.c +1/−1
• rts/idris_gmp.h +1/−1
• rts/idris_heap.c +12/−8
• rts/idris_heap.h +1/−1
• rts/idris_main.c +35/−3
• rts/idris_net.c +5/−0
• rts/idris_net.h +1/−0
• rts/idris_opts.c +1/−1
• rts/idris_opts.h +1/−1
• rts/idris_rts.c +24/−19
• rts/idris_rts.h +13/−10
• rts/idris_stdfgn.c +17/−7
• rts/windows/idris_net.c +5/−0
• rts/windows/win_utils.c +33/−3
• src/IRTS/CodegenC.hs +2/−1
• src/IRTS/CodegenCommon.hs +2/−0
• src/IRTS/Compiler.hs +23/−5
• src/IRTS/Lang.hs +2/−0
• src/IRTS/Portable.hs +88/−5
• src/IRTS/Simplified.hs +45/−50
• src/IRTS/System.hs +6/−1
• src/Idris/ASTUtils.hs +2/−1
• src/Idris/AbsSyntax.hs +156/−107
• src/Idris/AbsSyntaxTree.hs +100/−61
• src/Idris/Apropos.hs +2/−2
• src/Idris/CaseSplit.hs +23/−31
• src/Idris/CmdOptions.hs +49/−31
• src/Idris/Completion.hs +1/−0
• src/Idris/Core/Binary.hs +30/−11
• src/Idris/Core/CaseTree.hs +7/−7
• src/Idris/Core/Constraints.hs +1/−0
• src/Idris/Core/DeepSeq.hs +1/−0
• src/Idris/Core/Elaborate.hs +33/−34
• src/Idris/Core/Evaluate.hs +169/−69
• src/Idris/Core/Execute.hs +4/−4
• src/Idris/Core/ProofState.hs +60/−53
• src/Idris/Core/ProofTerm.hs +11/−11
• src/Idris/Core/TT.hs +106/−55
• src/Idris/Core/Typecheck.hs +141/−102
• src/Idris/Core/Unify.hs +61/−59
• src/Idris/Core/WHNF.hs +13/−13
• src/Idris/Coverage.hs +69/−33
• src/Idris/DataOpts.hs +1/−1
• src/Idris/DeepSeq.hs +1/−0
• src/Idris/Delaborate.hs +20/−20
• src/Idris/Docs.hs +10/−6
• src/Idris/Elab/Clause.hs +58/−95
• src/Idris/Elab/Data.hs +12/−8
• src/Idris/Elab/Implementation.hs +9/−16
• src/Idris/Elab/Interface.hs +164/−64
• src/Idris/Elab/Record.hs +4/−4
• src/Idris/Elab/Rewrite.hs +7/−7
• src/Idris/Elab/Term.hs +108/−76
• src/Idris/Elab/Transform.hs +3/−3
• src/Idris/Elab/Type.hs +9/−4
• src/Idris/Elab/Utils.hs +69/−36
• src/Idris/ElabDecls.hs +40/−13
• src/Idris/Erasure.hs +7/−7
• src/Idris/ErrReverse.hs +12/−4
• src/Idris/Error.hs +6/−0
• src/Idris/Help.hs +2/−0
• src/Idris/IBC.hs +41/−24
• src/Idris/IdrisDoc.hs +13/−14
• src/Idris/Info.hs +5/−0
• src/Idris/Interactive.hs +29/−32
• src/Idris/Main.hs +26/−19
• src/Idris/Package.hs +87/−29
• src/Idris/Parser.hs +18/−9
• src/Idris/Parser/Expr.hs +58/−53
• src/Idris/Parser/Helpers.hs +3/−3
• src/Idris/PartialEval.hs +19/−19
• src/Idris/Primitives.hs +5/−5
• src/Idris/ProofSearch.hs +8/−8
• src/Idris/Prover.hs +12/−12
• src/Idris/REPL.hs +54/−47
• src/Idris/REPL/Commands.hs +2/−0
• src/Idris/REPL/Parser.hs +11/−8
• src/Idris/Reflection.hs +15/−13
• src/Idris/Termination.hs +30/−31
• src/Idris/Transforms.hs +2/−2
• src/Idris/TypeSearch.hs +4/−4
• src/Util/System.hs +22/−2
• stack-shell.nix +1/−1
• stack.yaml +2/−2
• stylize.sh +39/−0
• test/TestData.hs +8/−4
• test/TestRun.hs +14/−8
• test/basic018/expected +1/−1
• test/basic019/basic019.idr +10/−0
• test/basic019/expected +12/−0
• test/basic019/run +4/−0
• test/dsl001/expected +4/−4
• test/dsl001/input +1/−1
• test/dsl001/run +2/−2
• test/dsl001/test001.idr +2/−0
• test/dsl002/Resimp.idr +1/−0
• test/dsl003/DSLPi.idr +2/−0
• test/dsl004/Door0.idr +3/−1
• test/dsl004/Door1.idr +2/−0
• test/dsl004/Door2.idr +2/−0
• test/dsl004/Door3.idr +2/−0
• test/dsl004/IOu.idr +2/−0
• test/interactive001/expected +1/−1
• test/interactive001/input +8/−8
• test/interactive001/interactive001.idr +45/−0
• test/interactive001/run +3/−1
• test/interactive001/test032.idr +0/−45
• test/interactive010/expected +2/−2
• test/interactive011/.gitignore +1/−0
• test/interactive011/input +2/−2
• test/interactive011/interactive011.idr +0/−11
• test/interactive011/interactive011.ipkg +8/−0
• test/interactive011/run +4/−1
• test/interactive011/src/Foo.idr +5/−0
• test/interactive011/src/Main.idr +14/−0
• test/interfaces002/interfaces002.idr +1/−4
• test/interfaces007/expected +1/−0
• test/interfaces007/interfaces007.idr +52/−0
• test/interfaces007/run +4/−0
• test/meta001/Finite.idr +2/−0
• test/meta002/AgdaStyleReflection.idr +1/−1
• test/meta002/DataDef.idr +2/−0
• test/meta002/Deriving.idr +2/−0
• test/meta002/Tacs.idr +1/−0
• test/meta002/expected +2/−2
• test/meta003/BadDef.idr +2/−0
• test/meta003/expected +1/−1
• test/meta004/expected +1/−1
• test/meta004/meta004.idr +2/−0
• test/pkg001/expected +1/−1
• test/pkg008/expected +13/−0
• test/pkg008/maths.ipkg +9/−0
• test/pkg008/run +9/−0
• test/pkg008/src/NumOps.idr +9/−0
• test/pkg008/src/Test.idr +21/−0
• test/proof002/Reflect.idr +1/−0
• test/proof002/expected +3/−3
• test/pruviloj001/pruviloj001.idr +1/−0
• test/regression001/reg002.idr +8/−0
• test/regression001/run +1/−1
• test/sourceLocation001/SourceLoc.idr +1/−0
• test/sourceLocation001/expected +8/−8
• test/tactics001/Tactics.idr +1/−1
• test/totality020/expected +1/−0
• test/totality020/run +3/−0
• test/totality020/totality020.idr +4/−0
• test/unique001/unique001.idr +2/−0
• test/unique004/expected +10/−10
• test/unique004/unique001a.idr +2/−0
• test/unique004/unique001b.idr +2/−0
• test/unique004/unique001c.idr +1/−0
• test/unique004/unique001d.idr +1/−0
• test/unique004/unique001e.idr +1/−0
• test/unique004/unique002.idr +2/−0
• test/unique004/unique002a.idr +2/−0
• test/unique004/unique003.idr +2/−0

@@ -0,0 +1,154 @@+# stylish-haskell configuration file+# ==================================++# The stylish-haskell tool is mainly configured by specifying steps. These steps+# are a list, so they have an order, and one specific step may appear more than+# once (if needed). Each file is processed by these steps in the given order.+steps:+  # Convert some ASCII sequences to their Unicode equivalents. This is disabled+  # by default.+  # - unicode_syntax:+  #     # In order to make this work, we also need to insert the UnicodeSyntax+  #     # language pragma. If this flag is set to true, we insert it when it's+  #     # not already present. You may want to disable it if you configure+  #     # language extensions using some other method than pragmas. Default:+  #     # true.+  #     add_language_pragma: true++  # Import cleanup+  - imports:+      # There are different ways we can align names and lists.+      #+      # - global: Align the import names and import list throughout the entire+      #   file.+      #+      # - file: Like global, but don't add padding when there are no qualified+      #   imports in the file.+      #+      # - group: Only align the imports per group (a group is formed by adjacent+      #   import lines).+      #+      # - none: Do not perform any alignment.+      #+      # Default: global.+      align: none++      # Folowing options affect only import list alignment.+      #+      # List align has following options:+      #+      # - after_alias: Import list is aligned with end of import including+      #   'as' and 'hiding' keywords.+      #+      #   > import qualified Data.List      as List (concat, foldl, foldr, head,+      #   >                                          init, last, length)+      #+      # - with_alias: Import list is aligned with start of alias or hiding.+      #+      #   > import qualified Data.List      as List (concat, foldl, foldr, head,+      #   >                                 init, last, length)+      #+      # - new_line: Import list starts always on new line.+      #+      #   > import qualified Data.List      as List+      #   >     (concat, foldl, foldr, head, init, last, length)+      #+      # Default: after_alias+      list_align: after_alias++      # Long list align style takes effect when import is too long. This is+      # determined by 'columns' setting.+      #+      # - inline: This option will put as much specs on same line as possible.+      #+      # - new_line: Import list will start on new line.+      #+      # - new_line_multiline: Import list will start on new line when it's+      #   short enough to fit to single line. Otherwise it'll be multiline.+      #+      # - multiline: One line per import list entry.+      #   Type with contructor list acts like single import.+      #+      #   > import qualified Data.Map as M+      #   >     ( empty+      #   >     , singleton+      #   >     , ...+      #   >     , delete+      #   >     )+      #+      # Default: inline+      long_list_align: inline++      # List padding determines indentation of import list on lines after import.+      # This option affects 'list_align' and 'long_list_align'.+      list_padding: 4++      # Separate lists option affects formating of import list for type+      # or class. The only difference is single space between type and list+      # of constructors, selectors and class functions.+      #+      # - true: There is single space between Foldable type and list of it's+      #   functions.+      #+      #   > import Data.Foldable (Foldable (fold, foldl, foldMap))+      #+      # - false: There is no space between Foldable type and list of it's+      #   functions.+      #+      #   > import Data.Foldable (Foldable(fold, foldl, foldMap))+      #+      # Default: true+      separate_lists: false++  # Language pragmas+  - language_pragmas:+      # We can generate different styles of language pragma lists.+      #+      # - vertical: Vertical-spaced language pragmas, one per line.+      #+      # - compact: A more compact style.+      #+      # - compact_line: Similar to compact, but wrap each line with+      #   `{-#LANGUAGE #-}'.+      #+      # Default: vertical.+      style: compact++      # Align affects alignment of closing pragma brackets.+      #+      # - true: Brackets are aligned in same collumn.+      #+      # - false: Brackets are not aligned together. There is only one space+      #   between actual import and closing bracket.+      #+      # Default: true+      align: true++      # stylish-haskell can detect redundancy of some language pragmas. If this+      # is set to true, it will remove those redundant pragmas. Default: true.+      remove_redundant: true++  # Align the types in record declarations+  # - records: {}++  # Replace tabs by spaces. This is disabled by default.+  - tabs:+  #     # Number of spaces to use for each tab. Default: 8, as specified by the+  #     # Haskell report.+      spaces: 8++  # Remove trailing whitespace+  - trailing_whitespace: {}++# A common setting is the number of columns (parts of) code will be wrapped+# to. Different steps take this into account. Default: 80.+columns: 80++# Sometimes, language extensions are specified in a cabal file or from the+# command line instead of using language pragmas in the file. stylish-haskell+# needs to be aware of these, so it can parse the file correctly.+#+# No language extensions are enabled by default.+# language_extensions:+  # - TemplateHaskell+  # - QuasiQuotes

@@ -8,6 +8,8 @@  matrix:   include:+    - env: CABALVER="1.24" GHCVER="8.0.1" STACKVER="7.14" STYLISH=YES+      addons: {apt: {packages: [cabal-install-1.24,ghc-8.0.1,hscolour], sources: [hvr-ghc]}}     - os: osx       env: CABALVER="1.24" GHCVER="8.0.1" TESTS="test_c"       compiler: ": #GHC 8.0.1"@@ -35,11 +37,17 @@     - 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]}}+  allow_failures:+    - os: osx+      env: CABALVER="1.24" GHCVER="8.0.1" TESTS="test_c"+      compiler: ": #GHC 8.0.1"+  fast-finish: true  cache:   directories:     - $HOME/.cabsnap     - $HOME/.cabal/packages+    - $HOME/.stack  before_cache:   - rm -fv $HOME/.cabal/packages/hackage.haskell.org/build-reports.log@@ -56,7 +64,6 @@   - env   - if [[ $TRAVIS_OS_NAME == 'osx' ]];     then-        brew update;         brew outdated pkgconfig || brew install pkgconfig;         brew install ghc cabal-install libffi cppcheck gnu-sed;         export PATH=$HOME/.cabal/bin:$PATH;@@ -64,8 +71,11 @@         export ZCAT=gzcat;         export PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig:$PKG_CONFIG_PATH;     fi+  - if [ -n "$STYLISH" ]; then ./stylize.sh; exit $?; fi  install:+  - which cabal+  - which ghc   - cabal --version   - echo "$(ghc --version) [$(ghc --print-project-git-commit-id 2> /dev/null || echo '?')]"   - if [ -f $HOME/.cabal/packages/hackage.haskell.org/00-index.tar.gz ];

@@ -1,3 +1,55 @@+# New in 0.99.1:++## Language updates++* Language pragmas now required for the less stable existing features, in+  addition to the existing `TypeProviders` and `ErrorReflection`:+  + `ElabReflection`, which must be enabled to use `%runElab`+  + `UniquenessTypes`, which must be enabled to use `UniqueType`+  + `DSLNotation`, which must be enabled to define a `dsl` block+  + `FirstClassReflection`, which must be enabled to define a `%reflection`+    function++* New language extension `LinearTypes`:+  + This allows adding a /multiplicity/ to a binder which says how often it+    is allowed to be used; either 0 or 1 (if unstated, multiplicity is "many")+  + The typing rules follow Conor McBride's paper "I Got Plenty o' Nuttin'"+  + This is highly experimental, unfinished, not at all polished. and there+    are still lots of details to sort out. Some features don't quite work+    properly yet. But it is there to play with for the brave!++## Tool Updates+++ Idris' output has been updated to more accurately reflect its+  progress through the compiler i.e. Type Checking; Totality Checking;+  IBC Generation; Compiling; and Code Generation. To control the+  loudness of the reporting three verbosity levels are introduced:+  `--V0`, `--V1`, and `--V2`. The old aliases of `-V` and `--verbose`+  persist.+++ New REPL command `:!` that runs an external shell command.+++ The REPL now colourises output on MinTTY consoles (e.g., Cygwin and MSYS)+  on Windows, which previously did not occur due to a bug.+++ Idris now runs in a UTF-8-compatible codepage on Windows. This fixes many+  Unicode-rendering issues on Windows (e.g., error messages stating+  `commitBuffer: invalid argument (invalid character)`).+++ Idris now has a `--warnipkg` flag to enable auditing of Idris+  packages during build time. Currently auditing check's the list of+  modules specified in the `iPKG` file with those presented in the+  package directory.++## Library Updates+++ Terminating programs has been improved with more appropriate+  functions (`exitWith`, `exitFailure`, and `exitSuccess`) and a data+  structure (`ExitCode`) to capture a program's return code.++ Casting a `String` to an `Int`, `Integer` or a `Double` now ignores leading+  and trailing whitespace. Previously only leading whitespace was ignored.++ RTS functions `openFile`, `do_popen`, and `ARGV` are now properly encoded using UTF-8 on Windows.+ # New in 0.99:  ## Language updates

@@ -42,6 +42,7 @@ Chao-Hong Chen Chetan Taralekar Chris Allen+Chris Gibbs Christopher Schwaab Cliff Harvey Cliff L. Biffle@@ -162,6 +163,7 @@ Norbert Melzer Oskar Wickström Ozgur Akgun+Patrick Hilhorst Patrik Jansson Paul Koerbitz Per Fredelius@@ -206,6 +208,7 @@ Trevor Elliott uwap Vitaly Bragilevsky+Vyacheslav Shebanov xged XIE Yuheng Yacine Hmito

@@ -1,3 +1,4 @@+{-# LANGUAGE TemplateHaskell #-} --  --------------------------------------------------------------- [ HLint.hs ] -- HLint suggestions we like. --

@@ -64,18 +64,28 @@ cross-platform program for developing Haskell projects, that enhances the functionality provided by Cabal. There is experimental support for building Idris from source with stack.+ This installation has been tested on Ubuntu 16.04.1 LTS, and the current NixOS unstable. -To build Idris with stack the following commands are recommended:+*Important* Stack will not install any external dependencies required+to build Idris. Before you try stack please ensure you have the+correct depenencies. +To build Idris with stack use the following command:+ * `stack build` -This will install Idris (and related executables) into `./local/bin/`-on Unix based systems and an appropriate place on Windows. If you-haven't used stack before this will also setup the related-infrastructure. For more information about Stack please visit the-[Stack website](https://github.com/commercialhaskell/stack).+To install Idris:++* `stack install`++Stack will install Idris (and related executables) into `$HOME/.local/bin/`+on Unix based systems and an appropriate place on Windows.++Of note: If you haven't used stack before commands will also setup the+related infrastructure. For more information about Stack please visit+the [Stack website](https://github.com/commercialhaskell/stack).  On NixOS, please use the following command instead, to make sure the required libraries and header files are available:

@@ -1,4 +1,4 @@-.PHONY: build configure doc install linecount nodefault pinstall lib_clean relib fast test_js test_c test test_clean lib_doc lib_doc_clean user_doc_html user_doc_pdf user_docs+.PHONY: build configure doc install linecount nodefault pinstall lib_clean relib fast test_js test_c stylize test test_clean lib_doc lib_doc_clean user_doc_html user_doc_pdf user_docs  ARGS= TEST-JOBS=@@ -24,7 +24,10 @@ build: dist/setup-config 	$(CABAL) build $(CABALFLAGS) -test: doc test_c+test: doc test_c stylize++stylize:+	./stylize.sh  test_c: 	$(CABAL) test $(ARGS) --test-options \

@@ -37,6 +37,7 @@ ## Announcements  + [ ] Update website.+  + [ ] Update web site with SHA256 hash of binary + [ ] Email Mailing list. + [ ] Make REDDIT post. + [ ] Tweet

@@ -1,4 +1,6 @@-ifneq (, $(findstring MSYS, $(shell uname -a)))+UNAME_INFO      := $(shell uname -a)++ifeq ($(filter , $(findstring MSYS, $(UNAME_INFO)) $(findstring MINGW, $(UNAME_INFO))),) 	ifeq (cc,$(CC)) 		# In MSYS2, when using the mingw version of gcc, there is no cc -> gcc 		# symlink. We can't use ?= here because CC is set implicitly to cc.

@@ -33,7 +33,7 @@ # ones. extensions = [     'sphinx.ext.todo',-    'sphinx.ext.pngmath',+    'sphinx.ext.pngmath', # imgmath is not supported on readthedocs.     'sphinx.ext.ifconfig', ] @@ -51,7 +51,7 @@  # General information about the project. project = u'Idris'-copyright = u'2015, The Idris Community'+copyright = u'2017, The Idris Community' author = u'The Idris Community'  # The version info for the project you're documenting, acts as replacement for@@ -59,9 +59,9 @@ # built documents. # # The short X.Y version.-version = '0.99'+version = '0.99.1' # The full version, including alpha/beta/rc tags.-release = '0.99'+release = '0.99.1'  # The language for content autogenerated by Sphinx. Refer to documentation # for a list of supported languages.

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

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

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

@@ -1,6 +1,6 @@-***********************-Compilation and Logging-***********************+************************************+Compilation, Logging, and Reporting+************************************  This section provides information about the Idris compilation process, and provides details over how you can follow the process through logging.@@ -41,11 +41,27 @@  Use of this option will still result in the generation of the Idris binary ``.ibc`` files, and is suitable if you do not wish to generate code from one of the supported backends. -Logging Output-==============+Reporting Compilation Process+============================= -The internal operation of Idris is captured using a category based logger.-Currently, the logging infrastructure has support for the following categories:+During compilation the reporting of Idris' progress can be controlled+by setting a verbosity level.+++ ``-V``, or alternatively ``--verbose`` and ``--V0``, will report which file Idris is currently type checking.++ ``--V1`` will additionally report: Parsing, IBC Generation, and Code+  Generation.++ ``--V2`` will additionally report: Totality Checking, Universe+  Checking, and the individual steps prior to code generation.+++By default Idris' progress reporting is set to quiet-``-q``, or ``--quiet``.++Logging Internal Operation+===========================++For those that develop on the Idris compiler, the internal operation+of Idris is captured using a category based logger. Currently, the+logging infrastructure has support for the following categories:  + Parser + Elaborator

@@ -61,7 +61,14 @@     ||| Add some numbers.     |||     ||| Addition is really great. This paragraph is not part of the overview.-    ||| Still the same paragraph. Lists are also nifty:+    ||| Still the same paragraph. +    |||+    ||| You can even provide examples which are inlined in the documentation:+    ||| ```idris example+    ||| add 4 5+    ||| ```+    ||| +    ||| Lists are also nifty:     ||| * Really nifty!     ||| * Yep!     ||| * The name `add` is a **bold** choice

@@ -164,7 +164,7 @@     myComparer = ...      qsort : Ptr -> Int -> Int -> IO ()-    test2 data elems elsize = foreign FFI_C "qsort"+    qsort data elems elsize = foreign FFI_C "qsort"                     (Ptr -> Int -> Int -> CFnPtr (Ptr -> Ptr -> Int) -> IO ())                     data elems elsize (MkCFnPtr myComparer) 

@@ -273,7 +273,7 @@   Existence of an implementation-========================+==============================  In order to show that an implementation of some interface is defined for some type, one could use the ``%implementation`` keyword:

@@ -97,7 +97,7 @@   which must be present for the package to be usable.  + ``objs = <objs>``, which takes a comma separated list of additional-  files to be installed (object files, headers), perhaps generated +  files to be installed (object files, headers), perhaps generated   by the ``Makefile``.  Testing@@ -112,6 +112,11 @@ .. IMPORTANT::   The modules containing the test functions must also be added to the list of modules. +Comments+---------++Package files support comments using the standard Idris singleline ``--`` and multiline ``{- -}`` format.+ Using Package files =================== @@ -127,9 +132,13 @@  + ``idris --mkdoc test.ipkg`` will build HTML documentation for your package in the folder ``test_doc`` in your project's root directory. ++ ``idris --installdoc test.ipkg`` will install the packages documentation into Idris' central documentation folder located at ``idris --docdir``.+ + ``idris --checkpkg test.ipkg`` will type check all modules in the package only. This differs from build that type checks **and** generates code.  + ``idris --testpkg test.ipkg`` will compile and run any embedded tests you have specified in the ``tests`` parameter.++When building or install packages the commandline flag ``--warnipkg`` will audit the project and warn of any potentiable problems.  Once the test package has been installed, the command line option ``--package test`` makes it accessible (abbreviated to ``-p test``).

@@ -158,6 +158,76 @@       Nil  : Vect Z a       (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a +The signature of type constructors may use dependent types++.. code:: idris++    data DPair : (a : Type) -> (a -> Type) -> Type where+      MkDPair : {P : a -> Type} -> (x : a) -> (pf : P x) -> DPair a P++Records+~~~~~~~++There is a special syntax for data types with one constructors and+multiple fields.++.. code:: idris++    record A a where+      constructor MkA+      foo, bar : a+      baz : Nat++This defines a constructor as well as getter and setter function for+each field.++.. code:: idris++    MkA : a -> a -> Nat -> A a+    foo : A a -> a+    set_foo : a -> A a -> A a++The types of record fields may depend on the value of other fields++.. code:: idris++    record Collection a where+      constructor MkCollection+      size : Nat+      items : Vect size a++Setter functions are only provided for fields that do not use dependant+types. In the example above neither ``set_size`` nor ``set_items`` are+defined.+++Co-data+~~~~~~~++Inifinite data structures can be introduced with the ``codata``+keyword.++.. code:: idris++  codata Stream : Type -> Type where+    (::) a -> Stream a -> Stream a++This is syntactic sugar for the following, which is usually preferred:++.. code:: idris++  data Stream : Type -> Type where+    (::) a -> Inf (Stream a) -> Stream a++Every occurence of the the defined type in a constructor argument will be+wrapped in the ``Inf`` type constructor. This has the effect of delaying the+evaluation of the second argument when the data constructor is applied.+An ``Inf`` argument is constructed using ``Delay`` (which Idris will insert+implicitly) adn evaluated using ``Force`` (again inserted implicitly).++Furthermore, recursive calls under a ``Delay`` must be guarded by a constructor+to pass the totality checker.+ Operators --------- 

@@ -24,7 +24,6 @@    interfaces    modules    packages-   testing    interp    views    theorems

@@ -153,6 +153,16 @@     sortAndShow : (Ord a, Show a) => List a -> String     sortAndShow xs = show (sort xs) +Note: Interfaces and ``mutual`` blocks+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~++Idris is strictly "define before use", except in ``mutual`` blocks.+In a ``mutual`` block, Idris elaborates in two passes: types on the first +pass and definitions on the second. When the mutual block contains an+interface declaration, it elaborates the interface header but none of the+method types on the first pass, and elaborates the method types and any+default definitions on the second pass.+ Functors and Applicatives ========================= 

@@ -299,3 +299,25 @@      *params> show (append _ _ (MkVects _ [1,2,3] [4,5,6]))     "[1, 2, 3, 4, 5, 6]" : String+++**********************+Modules Dependencies Using Atom +**********************++If you are using the Atom editor and have a dependency on another package, +corresponding to for instance ``import Lightyear`` or ``import Pruviloj``, +you need to let Atom know that it should be loaded. The easiest way to +accomplish that is with a .ipkg file. The general contents of an ipkg file +will be described in the next section of the tutorial, but for now here is +a simple recipe for this trivial case. ++- Create a folder myProject. ++- Add a file myProject.ipkg containing just a couple of lines: ++``package myProject`` ++``pkgs = pruviloj, lightyear`` ++- In Atom, use the File menu to Open Folder myProject. 

@@ -31,15 +31,19 @@   Other examples of package files can be found in the ``libs`` directory-of the main Idris repository, and in `third-party libraries <https://github.com/idris-lang/Idris-dev/wiki/Libraries>`_.-More details including a complete listing of available fields can be found in :ref:`ref-sect-packages`.+of the main Idris repository, and in `third-party libraries+<https://github.com/idris-lang/Idris-dev/wiki/Libraries>`_.   Using Package files =================== -Given an Idris package file ``maths.ipkg`` it can be used with the Idris compiler as follows: +Idris itself is aware about packages, and special commands are+available to help with, for example, building packages, installing+packages, and cleaning packages.  For instance, given the ``maths``+package from earlier we can use Idris as follows:+ + ``idris --build maths.ipkg`` will build all modules in the package  + ``idris --install maths.ipkg`` will install the package, making it@@ -48,20 +52,102 @@ + ``idris --clean maths.ipkg`` will delete all intermediate code and   executable files generated when building. -+ ``idris --mkdoc maths.ipkg`` will build HTML documentation for your-  package in the folder ``maths_doc`` in your project's root-  directory.--+ ``idris --checkpkg maths.ipkg`` will type check all modules in the-  package only. This differs from build that type checks **and**-  generates code.--+ ``idris --testpkg maths.ipkg`` will compile and run any embedded-  tests you have specified in the ``tests`` parameter. More-  information about testing is given in the next section.- Once the maths package has been installed, the command line option ``--package maths`` makes it accessible (abbreviated to ``-p maths``). For example::      idris -p maths Main.idr+++Testing Idris Packages+======================++The integrated build system includes a simple testing framework.+This framework collects functions listed in the ``ipkg`` file under ``tests``.+All test functions must return ``IO ()``.+++When you enter ``idris --testpkg yourmodule.ipkg``,+the build system creates a temporary file in a fresh environment on your machine+by listing the ``tests`` functions under a single ``main`` function.+It compiles this temporary file to an executable and then executes it.+++The tests themselves are responsible for reporting their success or failure.+Test functions commonly use ``putStrLn`` to report test results.+The test framework does not impose any standards for reporting and consequently+does not aggregate test results.+++For example, lets take the following list of functions that are defined in a module called ``NumOps`` for a sample package ``maths``.++.. name: Math/NumOps.idr+.. code-block:: idris++    module Maths.NumOps++    %access export -- to make functions under test visible++    double : Num a => a -> a+    double a = a + a++    triple : Num a => a -> a+    triple a = a + double a++A simple test module, with a qualified name of ``Test.NumOps`` can be declared as++.. name: Math/TestOps.idr+.. code-block:: idris++    module Test.NumOps++    import Maths.NumOps++    %access export  -- to make the test functions visible++    assertEq : Eq a => (given : a) -> (expected : a) -> IO ()+    assertEq g e = if g == e+        then putStrLn "Test Passed"+        else putStrLn "Test Failed"++    assertNotEq : Eq a => (given : a) -> (expected : a) -> IO ()+    assertNotEq g e = if not (g == e)+        then putStrLn "Test Passed"+        else putStrLn "Test Failed"++    testDouble : IO ()+    testDouble = assertEq (double 2) 4++    testTriple : IO ()+    testTriple = assertNotEq (triple 2) 5+++The functions ``assertEq`` and ``assertNotEq`` are used to run expected passing, and failing, equality tests.+The actual tests are ``testDouble`` and ``testTriple``, and are declared in the ``maths.ipkg`` file as follows::++    package maths++    modules = Maths.NumOps+            , Test.NumOps++    tests = Test.NumOps.testDouble+          , Test.NumOps.testTriple+++The testing framework can then be invoked using ``idris --testpkg maths.ipkg``::++    > idris --testpkg maths.ipkg+    Type checking ./Maths/NumOps.idr+    Type checking ./Test/NumOps.idr+    Type checking /var/folders/63/np5g0d5j54x1s0z12rf41wxm0000gp/T/idristests144128232716531729.idr+    Test Passed+    Test Passed++Note how both tests have reported success by printing ``Test Passed``+as we arranged for with the ``assertEq`` and ``assertNoEq`` functions.++More information+================++More details, including a complete listing of available fields, can be+found in the reference manual in :ref:`ref-sect-packages`.

@@ -92,7 +92,7 @@  .. code-block:: idris -    syntax for {x} in [xs] ":" [body] = forLoop xs (\x => body)+    syntax for {x} "in" [xs] ":" [body] = forLoop xs (\x => body)      main : IO ()     main = do for x in [1..10]:

@@ -1,85 +0,0 @@-.. _tut-sect-testing:--**********************-Testing Idris Packages-**********************--The integrated build system includes a simple testing framework.-This framework collects functions listed in the ``ipkg`` file under ``tests``.-All test functions must return ``IO ()``.---When you enter ``idris --testpkg yourmodule.ipkg``,-the build system creates a temporary file in a fresh environment on your machine-by listing the ``tests`` functions under a single ``main`` function.-It compiles this temporary file to an executable and then executes it.---The tests themselves are responsible for reporting their success or failure.-Test functions commonly use ``putStrLn`` to report test results.-The test framework does not impose any standards for reporting and consequently-does not aggregate test results.---For example, lets take the following list of functions that are defined in a module called ``NumOps`` for a sample package ``maths``.--.. name: Math/NumOps.idr-.. code-block:: idris--    module Maths.NumOps--    double : Num a => a -> a-    double a = a + a--    triple : Num a => a -> a-    triple a = a + double a--A simple test module, with a qualified name of ``Test.NumOps`` can be declared as--.. name: Math/TestOps.idr-.. code-block:: idris--    module Test.NumOps--    import Maths.NumOps--    assertEq : Eq a => (given : a) -> (expected : a) -> IO ()-    assertEq g e = if g == e-        then putStrLn "Test Passed"-        else putStrLn "Test Failed"--    assertNotEq : Eq a => (given : a) -> (expected : a) -> IO ()-    assertNotEq g e = if not (g == e)-        then putStrLn "Test Passed"-        else putStrLn "Test Failed"--    testDouble : IO ()-    testDouble = assertEq (double 2) 4--    testTriple : IO ()-    testTriple = assertNotEq (triple 2) 5---The functions ``assertEq`` and ``assertNotEq`` are used to run expected passing, and failing, equality tests.-The actual tests are ``testDouble`` and ``testTriple``, and are declared in the ``maths.ipkg`` file as follows::--    package maths--    modules = Maths.NumOps-            , Test.NumOps--    tests = Test.NumOps.testDouble-          , Test.NumOps.testTriple---The testing framework can then be invoked using ``idris --testpkg maths.ipkg``::--    > idris --testpkg maths.ipkg-    Type checking ./Maths/NumOps.idr-    Type checking ./Test/NumOps.idr-    Type checking /var/folders/63/np5g0d5j54x1s0z12rf41wxm0000gp/T/idristests144128232716531729.idr-    Test Passed-    Test Passed--Note how both tests have reported success by printing ``Test Passed``-as we arranged for with the ``assertEq`` and ``assertNoEq`` functions.

@@ -233,7 +233,7 @@ argument. The checker works by ensuring that all chains of recursive calls eventually lead to one of the arguments decreasing towards a base case, but sometimes this is hard to spot. For example, the following definition cannot be-checked as ``total`` because the checker cannot decide that ``filter (<= x) xs``+checked as ``total`` because the checker cannot decide that ``filter (< x) xs`` will always be smaller than ``(x :: xs)``:  .. code-block:: idris

@@ -713,7 +713,7 @@  .. code-block:: idris -    ones :: Stream Nat+    ones : Stream Nat     ones = 1 :: ones  It is important to note that codata does not allow the creation of infinite

@@ -1,5 +1,5 @@ Name:           idris-Version:        0.99+Version:        0.99.1 License:        BSD3 License-file:   LICENSE Author:         Edwin Brady@@ -259,10 +259,11 @@                 , array >= 0.4.0.1 && < 0.6                 , base64-bytestring < 1.1                 , binary >= 0.7 && < 0.9-                , blaze-html >= 0.6.1.3 && < 0.9-                , blaze-markup >= 0.5.2.1 && < 0.8+                , blaze-html >= 0.6.1.3 && < 0.10+                , blaze-markup >= 0.5.2.1 && < 0.9                 , bytestring < 0.11                 , cheapskate < 0.2+                , code-page >= 0.1 && < 0.2                 , containers >= 0.5 && < 0.6                 , deepseq < 1.5                 , directory >= 1.2.2.0 && < 1.2.3.0 || > 1.2.3.0@@ -289,7 +290,6 @@                 , vector < 0.12                 , vector-binary-instances < 0.3                 , zip-archive > 0.2.3.5 && < 0.4-                , safe == 0.3.9                 , fsnotify >= 0.2 && < 2.2                 , async < 2.2 @@ -302,6 +302,17 @@   else      build-depends: process < 1.5 +  -- safe 0.3.10 is having issues with cabal 1.20 and ghc 7.6.3, the+  -- hvr ghc ppa doesn't provide a new enough cabal library. Temporary+  -- fix until hvr ghc ppa is fixed or we deprecate support for 7.6.3.+  if impl(ghc < 7.8.4)+     build-depends: safe == 0.3.9+  else+     build-depends: safe >= 0.3.9++  if impl(ghc < 7.8.4)+     build-depends: tagsoup < 0.14.1+   Extensions:     MultiParamTypeClasses                 , DeriveFoldable                 , DeriveTraversable@@ -321,7 +332,8 @@   if os(darwin)      build-depends: unix < 2.8   if os(windows)-     build-depends: Win32 < 2.4+     build-depends: mintty >= 0.1 && < 0.2+                  , Win32 < 2.4   if flag(FFI)      build-depends: libffi < 0.2      cpp-options:   -DIDRIS_FFI

@@ -2,6 +2,7 @@  import Syntax.PreorderReasoning import Data.Fin+import Control.Category  %default total %access public export@@ -31,6 +32,10 @@         (\x => (from (from' (to' (to x))))  ={ cong (fromTo' (to x)) }=                (from (to x))                ={ fromTo x              }=                x                            QED)++Category Iso where+  id = isoRefl+  (.) = flip isoTrans  ||| Isomorphism is symmetric isoSym : Iso a b -> Iso b a

@@ -6,6 +6,9 @@                -- to improve it! (EB) %access export +||| Finds the next exponent of a power of two.+||| For example `nextPow2 200 = 8`, because 2^8 = 256.+||| If it is an exact match, it is not rounded up: `nextPow2 256 = 8` because 2^8 = 256. public export nextPow2 : Nat -> Nat nextPow2 Z = Z@@ -15,10 +18,17 @@     where       l2x = log2NZ (S x) SIsNotZ +||| Gets the lowest n for which "8 * 2 ^ n" is larger than or equal to the input.+||| For example, `nextBytes 10 = 16`.+||| Like with nextPow2, the result is not rounded up, so `nextBytes 16 = 16`. public export nextBytes : Nat -> Nat nextBytes bits = (nextPow2 (divCeilNZ bits 8 SIsNotZ)) +||| An index function to access the Bits* types in order.+||| machineTy 0 = Bits8, machineTy 1 = Bits16, etc.+||| Any input that would result in getting a type that is larger than supported+||| will result in the largest supported type instead (currently 64 bits). public export machineTy : Nat -> Type machineTy Z = Bits8@@ -26,9 +36,13 @@ machineTy (S (S Z)) = Bits32 machineTy (S (S (S _))) = Bits64 +||| Finds the number of bits used by `machineTy n`.+||| For example, bitsUsed 2 = 16 bitsUsed : Nat -> Nat bitsUsed n = 8 * (2 `power` n) +||| Converts a Nat to a machineTy n, with the first argument as an accumulator.+||| You shouldn't have to call this manually, use natToBits (without ') instead. natToBits' : %static {n : Nat} -> machineTy n -> Nat -> machineTy n natToBits' a Z = a natToBits' {n=n} a x with (n)@@ -39,6 +53,7 @@  natToBits' a (S x') | S (S (S _)) = natToBits' {n=3} (prim__addB64 a (prim__truncInt_B64 1)) x'  natToBits' a _      | _           = assert_unreachable +||| Converts a Nat to a machineTy n. natToBits : %static {n : Nat} -> Nat -> machineTy n natToBits {n=n} x with (n)     | Z           = natToBits' {n=0} (prim__truncInt_B8  0) x@@ -50,25 +65,36 @@ getPad : %static {n : Nat} -> Nat -> machineTy n getPad n = assert_total $ natToBits (minus (bitsUsed (nextBytes n)) n) +||| A "high-level" wrapper to the types defined by `machineTy`. public export data Bits : Nat -> Type where+    ||| An bits type that has at least n bits available,+    ||| up to the maximum supported by `machineTy`.     MkBits : machineTy (nextBytes n) -> Bits n -pad8 : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8+||| Perform a function over Bits8 as if it is carried out on n bits.+||| (n should be 8 or lower)+pad8 : (n : Nat) -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8 pad8 n f x y = prim__lshrB8 (f (prim__shlB8 x pad) (prim__shlB8 y pad)) pad     where       pad = getPad {n=0} n -pad16 : Nat -> (Bits16 -> Bits16 -> Bits16) -> Bits16 -> Bits16 -> Bits16+||| Perform a function over Bits16 as if it is carried out on n bits.+||| (n should be 16 or lower)+pad16 : (n: Nat) -> (Bits16 -> Bits16 -> Bits16) -> Bits16 -> Bits16 -> Bits16 pad16 n f x y = prim__lshrB16 (f (prim__shlB16 x pad) (prim__shlB16 y pad)) pad     where       pad = getPad {n=1} n +||| Perform a function over Bits32 as if it is carried out on n bits.+||| (n should be 32 or lower) pad32 : Nat -> (Bits32 -> Bits32 -> Bits32) -> Bits32 -> Bits32 -> Bits32 pad32 n f x y = prim__lshrB32 (f (prim__shlB32 x pad) (prim__shlB32 y pad)) pad     where       pad = getPad {n=2} n +||| Perform a function over Bits64 as if it is carried out on n bits.+||| (n should be 64 or lower) pad64 : Nat -> (Bits64 -> Bits64 -> Bits64) -> Bits64 -> Bits64 -> Bits64 pad64 n f x y = prim__lshrB64 (f (prim__shlB64 x pad) (prim__shlB64 y pad)) pad     where@@ -95,7 +121,7 @@     where       pad = getPad {n=3} n --- TODO: This (and all the other functions along these lings) is -- because it is used by things. Do they really need to be+-- TODO: This (and all the other functions along these lines) is -- because it is used by things. Do they really need to be -- public export, or is export good enough? shiftLeft' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n) shiftLeft' {n=n} x c with (nextBytes n)@@ -105,9 +131,11 @@     | S (S (S _)) = pad64' n prim__shlB64 x c     | _ = assert_unreachable +||| Binary left shift shiftLeft : %static {n : Nat} -> Bits n -> Bits n -> Bits n shiftLeft (MkBits x) (MkBits y) = MkBits (shiftLeft' x y) +||| Logical binary right shift shiftRightLogical' : %static {n : Nat} -> machineTy n -> machineTy n -> machineTy n shiftRightLogical' {n=n} x c with (n)     | Z = prim__lshrB8 x c@@ -116,10 +144,12 @@     | S (S (S _)) = prim__lshrB64 x c     | _ = assert_unreachable +||| Logical binary right shift shiftRightLogical : %static {n : Nat} -> Bits n -> Bits n -> Bits n shiftRightLogical {n} (MkBits x) (MkBits y)     = MkBits {n} (shiftRightLogical' {n=nextBytes n} x y) +||| Arithematic binary right shift shiftRightArithmetic' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n) shiftRightArithmetic' {n=n} x c with (nextBytes n)     | Z = pad8' n prim__ashrB8 x c@@ -128,9 +158,11 @@     | S (S (S _)) = pad64' n prim__ashrB64 x c     | _ = assert_unreachable +||| Arithematic binary right shift shiftRightArithmetic : %static {n : Nat} -> Bits n -> Bits n -> Bits n shiftRightArithmetic (MkBits x) (MkBits y) = MkBits (shiftRightArithmetic' x y) +||| Binary and and' : %static {n : Nat} -> machineTy n -> machineTy n -> machineTy n and' {n=n} x y with (n)     | Z = prim__andB8 x y@@ -139,9 +171,11 @@     | S (S (S _)) = prim__andB64 x y     | _ = assert_unreachable +||| Binary and and : %static {n : Nat} -> Bits n -> Bits n -> Bits n and {n} (MkBits x) (MkBits y) = MkBits (and' {n=nextBytes n} x y) +||| Binary or or' : %static {n : Nat} -> machineTy n -> machineTy n -> machineTy n or' {n=n} x y with (n)     | Z = prim__orB8 x y@@ -150,9 +184,11 @@     | S (S (S _)) = prim__orB64 x y     | _ = assert_unreachable +||| Binary or or : %static {n : Nat} -> Bits n -> Bits n -> Bits n or {n} (MkBits x) (MkBits y) = MkBits (or' {n=nextBytes n} x y) +||| Binary xor xor' : %static {n : Nat} -> machineTy n -> machineTy n -> machineTy n xor' {n=n} x y with (n)     | Z = prim__xorB8 x y@@ -161,9 +197,11 @@     | S (S (S _)) = prim__xorB64 x y     | _ = assert_unreachable +||| Binary xor xor : %static {n : Nat} -> Bits n -> Bits n -> Bits n xor {n} (MkBits x) (MkBits y) = MkBits {n} (xor' {n=nextBytes n} x y) +||| Overflowing addition plus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n) plus' {n=n} x y with (nextBytes n)     | Z = pad8 n prim__addB8 x y@@ -172,9 +210,11 @@     | S (S (S _)) = pad64 n prim__addB64 x y     | _ = assert_unreachable +||| Overflowing addition plus : %static {n : Nat} -> Bits n -> Bits n -> Bits n plus (MkBits x) (MkBits y) = MkBits (plus' x y) +||| Subtraction minus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n) minus' {n=n} x y with (nextBytes n)     | Z = pad8 n prim__subB8 x y@@ -183,9 +223,11 @@     | S (S (S _)) = pad64 n prim__subB64 x y     | _ = assert_unreachable +||| Subtraction minus : %static {n : Nat} -> Bits n -> Bits n -> Bits n minus (MkBits x) (MkBits y) = MkBits (minus' x y) +||| Multiplication times' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n) times' {n=n} x y with (nextBytes n)     | Z = pad8 n prim__mulB8 x y@@ -194,9 +236,11 @@     | S (S (S _)) = pad64 n prim__mulB64 x y     | _ = assert_unreachable +||| Multiplication times : %static {n : Nat} -> Bits n -> Bits n -> Bits n times (MkBits x) (MkBits y) = MkBits (times' x y) +||| Signed integer division partial sdiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n) sdiv' {n=n} x y with (nextBytes n)@@ -206,10 +250,12 @@     | S (S (S _)) = prim__sdivB64 x y     | _ = assert_unreachable +||| Signed integer division partial sdiv : %static {n : Nat} -> Bits n -> Bits n -> Bits n sdiv (MkBits x) (MkBits y) = MkBits (sdiv' x y) +||| Unsigned integer division partial udiv' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n) udiv' {n=n} x y with (nextBytes n)@@ -219,10 +265,12 @@     | S (S (S _)) = prim__udivB64 x y     | _ = assert_unreachable +||| Unsigned integer division partial udiv : %static {n : Nat} -> Bits n -> Bits n -> Bits n udiv (MkBits x) (MkBits y) = MkBits (udiv' x y) +||| Signed remainder (mod) partial srem' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n) srem' {n=n} x y with (nextBytes n)@@ -232,10 +280,12 @@     | S (S (S _)) = prim__sremB64 x y     | _ = assert_unreachable +||| Signed remainder (mod) partial srem : %static {n : Nat} -> Bits n -> Bits n -> Bits n srem (MkBits x) (MkBits y) = MkBits (srem' x y) +||| Unsigned remainder (mod) partial urem' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n) urem' {n=n} x y with (nextBytes n)@@ -245,6 +295,7 @@     | S (S (S _)) = prim__uremB64 x y     | _ = assert_unreachable +||| Unsigned remainder (mod) partial urem : %static {n : Nat} -> Bits n -> Bits n -> Bits n urem (MkBits x) (MkBits y) = MkBits (urem' x y)@@ -447,4 +498,3 @@  implementation Show (Bits n) where     show = bitsToStr-

@@ -63,15 +63,23 @@ implementation Functor Complex where     map f (r :+ i) = f r :+ f i --- We can't do "implementation Num a => Num (Complex a)" because--- we need "abs" which needs "magnitude" which needs "sqrt" which needs Double-implementation Num (Complex Double) where+-- We can do "implementation Neg a => Num (Complex a)" because+-- we don't need "abs", only (-)+implementation Neg a => Num (Complex a) where     (+) (a:+b) (c:+d) = ((a+c):+(b+d))     (*) (a:+b) (c:+d) = ((a*c-b*d):+(b*c+a*d))     fromInteger x = (fromInteger x:+0) +-- We can't do "implementation Neg a => Neg (Complex a)" because+-- we need "abs" which needs "magnitude" which needs "sqrt" which needs Double implementation Neg (Complex Double) where     negate = map negate     (-) (a:+b) (c:+d) = ((a-c):+(b-d))     abs (a:+b) = (magnitude (a:+b):+0) +-- As soon as abs moves out of Neg (issue #3500), the following would become a+-- valid instance:++-- implementation Neg a => Neg (Complex a) where+--     negate = map negate+--     (-) (a:+b) (c:+d) = ((a-c):+(b-d))

@@ -225,5 +225,3 @@   vList (ys ++ zs) | (MkSplitBal prf)          = toVList ys (snocList zs) prf --

@@ -1,5 +1,7 @@ module Data.String.Views +%access public export+ ||| View for traversing a String one character at a time data StrList : String -> Type where      SNil  : StrList ""

@@ -12,9 +12,6 @@         (message : String) ->         a error {loc = FileLoc filename (line, col) _} message =-  believe_me . unsafePerformIO $ -    do let place = filename ++ " line " ++ show line ++ " column " ++ show col-       let message' = place ++ ": " ++ message-       putStrLn message'-       exit 1-+    let place = filename ++ " line " ++ show line ++ " column " ++ show col+        message' = place ++ ": " ++ message in+        idris_crash message'

@@ -264,6 +264,18 @@           equalp (UType u)    (UType u')       = u == u'           equalp x            y                = False +implementation Eq Raw where+  a == b = equalp a b+    where equalp : Raw -> Raw -> Bool+          equalp (Var x)         (Var y)         = assert_total $ x == y+          equalp (RBind x b1 e1) (RBind y b2 e2) = assert_total $ x == y && b1 == b2 && e1 == e2+          equalp (RApp f1 a1)    (RApp f2 a2)    = assert_total $ f1 == f2 && a1 == a2+          equalp RType           RType           = True+          equalp (RUType u1)     (RUType u2)     = u1 == u2+          equalp (RConstant c1)  (RConstant c2)  = c1 == c2+          equalp _               _               = False++ total forget : TT -> Maybe Raw forget tm = fe [] tm

@@ -1,5 +1,7 @@ module System +import public Data.So+ %include C "unistd.h" %default partial %access public export@@ -52,18 +54,48 @@          then pure $ reverse $ map splitEq acc          else getAllPairs (n + 1) (envPair :: acc) +||| Programs can either terminate successfully, or end in a caught+||| failure.+data ExitCode : Type where+  ||| Terminate successfully.+  ExitSuccess : ExitCode+  ||| Program terminated for some prescribed reason.+  |||+  ||| @errNo A non-zero numerical value indicating failure.+  ||| @prf   Proof that the int value is non-zero.+  ExitFailure : (errNo    : Int)+             -> {auto prf : So (not $ errNo == 0)}+             -> ExitCode+ ||| Quit with a particular exit code-exit : Int -> IO ()-exit code = foreign FFI_C "exit" (Int -> IO ()) code+exit : Int -> IO a+exit code = believe_me $ foreign FFI_C "exit" (Int -> IO ()) code -||| Get the numbers of seconds since 1st January 1970, 00:00 UTC +||| Terminate the program with an `ExitCode`. This code indicates the+||| success of the program's execution, and returns the success code+||| to the program's caller.+|||+||| @code The `ExitCode` for program.+exitWith : (code : ExitCode) -> IO a+exitWith ExitSuccess         = exit 0+exitWith (ExitFailure errNo) = exit errNo++||| Exit the program indicating failure.+exitFailure : IO a+exitFailure = exitWith (ExitFailure 1)++||| Exit the program after a successful run.+exitSuccess : IO a+exitSuccess = exitWith ExitSuccess++||| Get the numbers of seconds since 1st January 1970, 00:00 UTC time : IO Integer time = do MkRaw t <- foreign FFI_C "idris_time" (IO (Raw Integer))           pure t -usleep : Int -> IO ()+||| Specify interval to sleep for, must be in range [0, 1000000]+usleep : (i : Int) -> { auto prf : So (i >= 0 && i <= 1000000) } -> IO () usleep i = foreign FFI_C "usleep" (Int -> IO ()) i  system : String -> IO Int system cmd = foreign FFI_C "system" (String -> IO Int) cmd-

@@ -1,6 +1,6 @@ package base -opts = "--nobasepkgs --total --no-elim-deprecation-warnings -i ../prelude"+opts = "--nobasepkgs --total --no-elim-deprecation-warnings --partial-eval -i ../prelude" modules = System,            Debug.Error, Debug.Trace,

@@ -126,13 +126,15 @@         offsets' [] acc _ = reverse acc         offsets' (x::xs) acc pos = offsets' xs (pos::acc) (sizeOf x) +%language ElabReflection -- needed for 'error', which finds a line number+ private indexOrFail : Nat -> List a -> a indexOrFail i xs = case index' i xs of                         Just x => x                         Nothing => error "Out of bounds access" -||| The offset of a firld in a composite type+||| The offset of a field in a composite type export offset : Composite -> Nat -> Int offset (STRUCT xs) i = indexOrFail i (offsetsStruct xs)

@@ -0,0 +1,541 @@+module Control.ST++import Language.Reflection.Utils++%default total++infix 5 :::++{- A resource is a pair of a label and the current type stored there -}+public export+data Resource : Type where+     MkRes : label -> Type -> Resource++%error_reverse+public export+(:::) : label -> Type -> Resource+(:::) = MkRes++export+data Var = MkVar -- Phantom, just for labelling purposes++{- Contexts for holding current resources states -}+namespace Context+  public export+  data Context : Type where+       Nil : Context+       (::) : Resource -> Context -> Context++  public export+  (++) : Context -> Context -> Context+  (++) [] ys = ys+  (++) (x :: xs) ys = x :: xs ++ ys++{- Proof that a label has a particular type in a given context -}+public export+data InState : lbl -> Type -> Context -> Type where+     Here : InState lbl st (MkRes lbl st :: rs)+     There : InState lbl st rs -> InState lbl st (r :: rs)++{- Update an entry in a context with a new state -}+public export+updateCtxt : (ctxt : Context) -> +             InState lbl st ctxt -> Type -> Context+updateCtxt (MkRes lbl _ :: rs) Here val = (MkRes lbl val :: rs)+updateCtxt (r :: rs) (There x) ty = r :: updateCtxt rs x ty++{- Remove an entry from a context -}+public export+drop : (ctxt : Context) -> (prf : InState lbl st ctxt) -> +       Context+drop (MkRes lbl st :: rs) Here = rs+drop (r :: rs) (There p) = r :: drop rs p++{- Proof that a resource state (label/type) is in a context -}+public export+data ElemCtxt : Resource -> Context -> Type where+     HereCtxt : ElemCtxt a (a :: as)+     ThereCtxt : ElemCtxt a as -> ElemCtxt a (b :: as)++public export %error_reduce+dropEl : (ys: _) -> ElemCtxt x ys -> Context+dropEl (x :: as) HereCtxt = as+dropEl (x :: as) (ThereCtxt p) = x :: dropEl as p++{- Proof that a variable name is in a context -}+public export+data VarInCtxt : Var -> Context -> Type where+     VarHere   : VarInCtxt a (MkRes a st :: as)+     VarThere  : VarInCtxt a as -> VarInCtxt a (b :: as)++public export %error_reduce+dropVarIn : (ys: _) -> VarInCtxt x ys -> Context+dropVarIn ((MkRes x _) :: as) VarHere = as+dropVarIn (x :: as) (VarThere p) = x :: dropVarIn as p++public export+data Composite : List Type -> Type where+     CompNil : Composite []+     CompCons : (x : a) -> Composite as -> Composite (a :: as)++namespace VarList+  public export+  data VarList : List Type -> Type where+       Nil : VarList []+       (::) : Var -> VarList ts -> VarList (t :: ts)++  public export+  mkCtxt : VarList tys -> Context+  mkCtxt [] = []+  mkCtxt {tys = (t :: ts)} (v :: vs) = (v ::: t) :: mkCtxt vs++{- Proof that a context is a subset of another context -}+public export+data SubCtxt : Context -> Context -> Type where+     SubNil : SubCtxt [] []+     InCtxt : (el : ElemCtxt x ys) -> SubCtxt xs (dropEl ys el) ->+              SubCtxt (x :: xs) ys+     Skip : SubCtxt xs ys -> SubCtxt xs (y :: ys)++%hint+public export+subCtxtId : SubCtxt xs xs+subCtxtId {xs = []} = SubNil+subCtxtId {xs = (x :: xs)} = InCtxt HereCtxt subCtxtId++public export+subCtxtNil : SubCtxt [] xs+subCtxtNil {xs = []} = SubNil+subCtxtNil {xs = (x :: xs)} = Skip subCtxtNil++{- Proof that every variable in the list appears once in the context -}+public export+data VarsIn : List Var -> Context -> Type where+     VarsNil : VarsIn [] []+     InCtxtVar : (el : VarInCtxt x ys) -> VarsIn xs (dropVarIn ys el) ->+                 VarsIn (x :: xs) ys+     SkipVar : VarsIn xs ys -> VarsIn xs (y :: ys)++public export+Uninhabited (ElemCtxt x []) where+  uninhabited HereCtxt impossible+  uninhabited (ThereCtxt _) impossible++public export %error_reduce+updateWith : (new : Context) -> (xs : Context) ->+             SubCtxt ys xs -> Context+-- At the end, add the ones which were updated by the subctxt+updateWith new [] SubNil = new+updateWith new [] (InCtxt el z) = absurd el+-- Don't add the ones which were consumed by the subctxt+updateWith [] (x :: xs) (InCtxt el p) +    = updateWith [] (dropEl _ el) p+updateWith (n :: ns) (x :: xs) (InCtxt el p) +    = n :: updateWith ns (dropEl _ el) p+-- Do add the ones we didn't use in the subctxt+updateWith new (x :: xs) (Skip p) = x :: updateWith new xs p++public export+getVarType : (xs : Context) -> VarInCtxt v xs -> Type+getVarType ((MkRes v st) :: as) VarHere = st+getVarType (b :: as) (VarThere x) = getVarType as x++public export+getCombineType : VarsIn ys xs -> List Type+getCombineType VarsNil = []+getCombineType (InCtxtVar el y) = getVarType _ el :: getCombineType y+getCombineType (SkipVar x) = getCombineType x++public export+dropCombined : VarsIn vs ctxt -> Context+dropCombined {ctxt = []} VarsNil = []+dropCombined {ctxt} (InCtxtVar el y) = dropCombined y+dropCombined {ctxt = (y :: ys)} (SkipVar x) = y :: dropCombined x++public export+combineVarsIn : (ctxt : Context) -> VarsIn (comp :: vs) ctxt -> Context+combineVarsIn {comp} ctxt (InCtxtVar el x) +     = ((comp ::: Composite (getCombineType x)) :: dropCombined (InCtxtVar el x))+combineVarsIn (y :: ys) (SkipVar x) = y :: combineVarsIn ys x++namespace Env+  public export+  data Env : Context -> Type where+       Nil : Env []+       (::) : ty -> Env xs -> Env ((lbl ::: ty) :: xs)++lookupEnv : InState lbl ty ctxt -> Env ctxt -> ty+lookupEnv Here (x :: xs) = x+lookupEnv (There p) (x :: xs) = lookupEnv p xs++updateEnv : (prf : InState lbl ty ctxt) -> Env ctxt -> ty' -> +            Env (updateCtxt ctxt prf ty')+updateEnv Here (x :: xs) val = val :: xs+updateEnv (There p) (x :: xs) val = x :: updateEnv p xs val++dropVal : (prf : InState lbl st ctxt) -> Env ctxt -> Env (drop ctxt prf)+dropVal Here (x :: xs) = xs+dropVal (There p) (x :: xs) = x :: dropVal p xs++envElem : ElemCtxt x xs -> Env xs -> Env [x]+envElem HereCtxt (x :: xs) = [x]+envElem (ThereCtxt p) (x :: xs) = envElem p xs++dropDups : Env xs -> (el : ElemCtxt x xs) -> Env (dropEl xs el)+dropDups (y :: ys) HereCtxt = ys+dropDups (y :: ys) (ThereCtxt p) = y :: dropDups ys p+++dropEntry : Env ctxt -> (prf : VarInCtxt x ctxt) -> Env (dropVarIn ctxt prf)+dropEntry (x :: env) VarHere = env+dropEntry (x :: env) (VarThere y) = x :: dropEntry env y++dropVarsIn : Env ctxt -> (prf : VarsIn vs ctxt) -> Env (dropCombined prf)+dropVarsIn [] VarsNil = []+dropVarsIn env (InCtxtVar el z) = dropVarsIn (dropEntry env el) z+dropVarsIn (x :: env) (SkipVar z) = x :: dropVarsIn env z++getVarEntry : Env ctxt -> (prf : VarInCtxt v ctxt) -> getVarType ctxt prf+getVarEntry (x :: xs) VarHere = x+getVarEntry (x :: env) (VarThere p) = getVarEntry env p++mkComposite : Env ctxt -> (prf : VarsIn vs ctxt) -> Composite (getCombineType prf)+mkComposite [] VarsNil = CompNil+mkComposite env (InCtxtVar el z) +    = CompCons (getVarEntry env el) (mkComposite (dropEntry env el) z)+mkComposite (x :: env) (SkipVar z) = mkComposite env z++rebuildVarsIn : Env ctxt -> (prf : VarsIn (comp :: vs) ctxt) -> +                Env (combineVarsIn ctxt prf)+rebuildVarsIn env (InCtxtVar el p) +     = mkComposite (dropEntry env el) p :: dropVarsIn env (InCtxtVar el p)+rebuildVarsIn (x :: env) (SkipVar p) = x :: rebuildVarsIn env p++{- Some things to make STrans interfaces look prettier -}++infix 6 :->+          +public export+data Action : Type -> Type where+     Stable : lbl -> Type -> Action ty+     Trans : lbl -> Type -> (ty -> Type) -> Action ty+     Remove : lbl -> Type -> Action ty+     Add : (ty -> Context) -> Action ty++namespace Stable+  public export %error_reduce+  (:::) : lbl -> Type -> Action ty+  (:::) = Stable++namespace Trans+  public export+  data Trans ty = (:->) Type Type++  public export %error_reduce+  (:::) : lbl -> Trans ty -> Action ty+  (:::) lbl (st :-> st') = Trans lbl st (const st')++namespace DepTrans+  public export+  data DepTrans ty = (:->) Type (ty -> Type)++  public export %error_reduce+  (:::) : lbl -> DepTrans ty -> Action ty+  (:::) lbl (st :-> st') = Trans lbl st st'++public export+or : a -> a -> Either b c -> a+or x y = either (const x) (const y)++public export+add : Type -> Action a+add ty = Add (\var => [var ::: ty])++public export+addIfRight : Type -> Action (Either a b)+addIfRight ty = Add (either (const []) (\var => [var ::: ty]))++public export+addIfJust : Type -> Action (Maybe a)+addIfJust ty = Add (maybe [] (\var => [var ::: ty]))++public export+kept : SubCtxt xs ys -> Context+kept SubNil = []+kept (InCtxt el p) = kept p+kept (Skip {y} p) = y :: kept p++-- We can only use new/delete/read/write on things wrapped in State. Only an+-- interface implementation should know that a thing is defined as State,+-- so it's the only thing that's able to peek at the internals+public export+data State : Type -> Type where+     Value : ty -> State ty++export+data STrans : (m : Type -> Type) ->+              (ty : Type) ->+              Context -> (ty -> Context) ->+              Type where+     Pure : (result : ty) -> +            STrans m ty (out_fn result) out_fn+     Bind : STrans m a st1 st2_fn ->+            ((result : a) -> +                STrans m b (st2_fn result) st3_fn) ->+            STrans m b st1 st3_fn+     Lift : Monad m => m t -> STrans m t ctxt (const ctxt)++     New : (val : state) -> +           STrans m Var ctxt (\lbl => (lbl ::: state) :: ctxt)+     Delete : (lbl : Var) ->+              (prf : InState lbl st ctxt) ->+              STrans m () ctxt (const (drop ctxt prf))+     DropSubCtxt : (prf : SubCtxt ys xs) ->+                   STrans m (Env ys) xs (const (kept prf))++     Split : (lbl : Var) ->+             (prf : InState lbl (Composite vars) ctxt) ->+             STrans m (VarList vars) ctxt +                   (\ vs => mkCtxt vs ++ +                            updateCtxt ctxt prf (State ()))+     Combine : (comp : Var) -> (vs : List Var) ->+               (prf : VarsIn (comp :: vs) ctxt) ->+               STrans m () ctxt+                   (const (combineVarsIn ctxt prf))++     Call : STrans m t sub new_f -> (ctxt_prf : SubCtxt sub old) ->+            STrans m t old (\res => updateWith (new_f res) old ctxt_prf)++     Read : (lbl : Var) ->+            (prf : InState lbl ty ctxt) ->+            STrans m ty ctxt (const ctxt)+     Write : (lbl : Var) ->+             (prf : InState lbl ty ctxt) ->+             (val : ty') ->+             STrans m () ctxt (const (updateCtxt ctxt prf ty'))++export+dropEnv : Env ys -> SubCtxt xs ys -> Env xs+dropEnv [] SubNil = []+dropEnv [] (InCtxt idx rest) = absurd idx+dropEnv (z :: zs) (InCtxt idx rest) +    = let [e] = envElem idx (z :: zs) in+          e :: dropEnv (dropDups (z :: zs) idx) rest+dropEnv (z :: zs) (Skip p) = dropEnv zs p++keepEnv : Env ys -> (prf : SubCtxt xs ys) -> Env (kept prf)+keepEnv env SubNil = env+keepEnv env (InCtxt el prf) = keepEnv (dropDups env el) prf+keepEnv (z :: zs) (Skip prf) = z :: keepEnv zs prf++-- Corresponds pretty much exactly to 'updateWith'+rebuildEnv : Env new -> Env old -> (prf : SubCtxt sub old) ->+             Env (updateWith new old prf)+rebuildEnv new [] SubNil = new+rebuildEnv new [] (InCtxt el p) = absurd el+rebuildEnv [] (x :: xs) (InCtxt el p) +    = rebuildEnv [] (dropDups (x :: xs) el) p+rebuildEnv (e :: es) (x :: xs) (InCtxt el p) +    = e :: rebuildEnv es (dropDups (x :: xs) el) p+rebuildEnv new (x :: xs) (Skip p) = x :: rebuildEnv new xs p++runST : Env invars -> STrans m a invars outfn ->+        ((x : a) -> Env (outfn x) -> m b) -> m b+runST env (Pure result) k = k result env+runST env (Bind prog next) k +   = runST env prog (\prog', env' => runST env' (next prog') k)+runST env (Lift action) k +   = do res <- action+        k res env+runST env (New val) k = k MkVar (val :: env)+runST env (Delete lbl prf) k = k () (dropVal prf env)+runST env (DropSubCtxt prf) k = k (dropEnv env prf) (keepEnv env prf)+runST env (Split lbl prf) k = let val = lookupEnv prf env +                                  env' = updateEnv prf env (Value ()) in+                                  k (mkVars val) (addToEnv val env')+  where+    mkVars : Composite ts -> VarList ts+    mkVars CompNil = []+    mkVars (CompCons x xs) = MkVar :: mkVars xs++    addToEnv : (comp : Composite ts) -> Env xs -> Env (mkCtxt (mkVars comp) ++ xs)+    addToEnv CompNil env = env+    addToEnv (CompCons x xs) env = x :: addToEnv xs env+runST env (Combine lbl vs prf) k = k () (rebuildVarsIn env prf)+runST env (Call prog ctxt_prf) k +   = let env' = dropEnv env ctxt_prf in+         runST env' prog+                 (\prog', envk => k prog' (rebuildEnv envk env ctxt_prf))+runST env (Read lbl prf) k = k (lookupEnv prf env) env+runST env (Write lbl prf val) k = k () (updateEnv prf env val)+++export +pure : (result : ty) -> STrans m ty (out_fn result) out_fn+pure = Pure+ +export +(>>=) : STrans m a st1 st2_fn ->+        ((result : a) -> STrans m b (st2_fn result) st3_fn) ->+        STrans m b st1 st3_fn+(>>=) = Bind++export+lift : Monad m => m t -> STrans m t ctxt (const ctxt)+lift = Lift++export+new : (val : state) -> +      STrans m Var ctxt (\lbl => (lbl ::: State state) :: ctxt)+new val = New (Value val)++export+delete : (lbl : Var) ->+         {auto prf : InState lbl (State st) ctxt} ->+         STrans m () ctxt (const (drop ctxt prf))+delete lbl {prf} = Delete lbl prf++-- Keep only a subset of the current set of resources. Returns the+-- environment corresponding to the dropped portion.+export+dropSubCtxt : {auto prf : SubCtxt ys xs} ->+              STrans m (Env ys) xs (const (kept prf))+dropSubCtxt {prf} = DropSubCtxt prf++export+split : (lbl : Var) ->+        {auto prf : InState lbl (Composite vars) ctxt} ->+        STrans m (VarList vars) ctxt +              (\ vs => mkCtxt vs ++ +                       updateCtxt ctxt prf (State ()))+split lbl {prf} = Split lbl prf++export+combine : (comp : Var) -> (vs : List Var) ->+          {auto prf : InState comp (State ()) ctxt} ->+          {auto var_prf : VarsIn (comp :: vs) ctxt} ->+          STrans m () ctxt+              (const (combineVarsIn ctxt var_prf))+combine comp vs {var_prf} = Combine comp vs var_prf++export -- implicit ???+call : STrans m t sub new_f ->+       {auto ctxt_prf : SubCtxt sub old} ->+       STrans m t old (\res => updateWith (new_f res) old ctxt_prf)+call prog {ctxt_prf} = Call prog ctxt_prf+ +export+read : (lbl : Var) ->+       {auto prf : InState lbl (State ty) ctxt} ->+       STrans m ty ctxt (const ctxt)+read lbl {prf} = do Value x <- Read lbl prf+                    pure x++export+write : (lbl : Var) ->+        {auto prf : InState lbl ty ctxt} ->+        (val : ty') ->+        STrans m () ctxt (const (updateCtxt ctxt prf (State ty')))+write lbl {prf} val = Write lbl prf (Value val)+    +public export %error_reduce+out_res : ty -> (as : List (Action ty)) -> Context+out_res x [] = []+out_res x ((Stable lbl inr) :: xs) = (lbl ::: inr) :: out_res x xs+out_res x ((Trans lbl inr outr) :: xs) +    = (lbl ::: outr x) :: out_res x xs+out_res x ((Remove lbl inr) :: xs) = out_res x xs+out_res x (Add outf :: xs) = outf x ++ out_res x xs++public export %error_reduce+in_res : (as : List (Action ty)) -> Context+in_res [] = []+in_res ((Stable lbl inr) :: xs) = (lbl ::: inr) :: in_res xs+in_res ((Trans lbl inr outr) :: xs) = (lbl ::: inr) :: in_res xs+in_res ((Remove lbl inr) :: xs) = (lbl ::: inr) :: in_res xs+in_res (Add outf :: xs) = in_res xs++public export+%error_reduce -- always evaluate this before showing errors+ST : (m : Type -> Type) ->+     (ty : Type) -> +     List (Action ty) -> Type+ST m ty xs = STrans m ty (in_res xs) (\result : ty => out_res result xs)++-- Console IO is useful sufficiently often that let's have it here+public export+interface ConsoleIO (m : Type -> Type) where+  putStr : String -> STrans m () xs (const xs)+  getStr : STrans m String xs (const xs)++export+ConsoleIO IO where+  putStr str = lift (Interactive.putStr str)+  getStr = lift Interactive.getLine+++export+run : Applicative m => ST m a [] -> m a+run prog = runST [] prog (\res, env' => pure res)++||| runWith allows running an STrans program with an initial environment,+||| which must be consumed.+||| It's only allowed in the IO monad, because it's inherently unsafe, so+||| we don't want to be able to use it under a 'lift in just *any* ST program -+||| if we have access to an 'Env' we can easily duplicate it - so it's the+||| responsibility of an implementation of an interface in IO which uses it+||| to ensure that it isn't duplicated.+export+runWith : {ctxtf : _} ->+          Env ctxt -> STrans IO a ctxt (\res => ctxtf res) -> +          IO (res ** Env (ctxtf res))+runWith env prog = runST env prog (\res, env' => pure (res ** env'))++export+runPure : ST Basics.id a [] -> a+runPure prog = runST [] prog (\res, env' => res)++%language ErrorReflection++%error_handler+export+st_precondition : Err -> Maybe (List ErrorReportPart)+st_precondition (CantSolveGoal `(SubCtxt ~sub ~all) _)+   = pure +      [TextPart "'call' is not valid here. ",+       TextPart "The operation has preconditions ",+       TermPart sub,+       TextPart " which is not a sub set of ",+       TermPart all]+st_precondition (CantUnify _ tm1 tm2 _ _ _)+   = do reqPre <- getPreconditions tm1+        gotPre <- getPreconditions tm2+        reqPost <- getPostconditions tm1+        gotPost <- getPostconditions tm2+        pure $ [TextPart "Error in state transition:"] +++                renderPre gotPre reqPre +++                renderPost gotPost reqPost++  where+    getPreconditions : TT -> Maybe TT+    getPreconditions `(STrans ~m ~ret ~pre ~post) = Just pre+    getPreconditions _ = Nothing++    getPostconditions : TT -> Maybe TT+    getPostconditions `(STrans ~m ~ret ~pre ~post) = Just post+    getPostconditions _ = Nothing++    renderPre : TT -> TT -> List (ErrorReportPart)+    renderPre got req +        = [SubReport [TextPart "Operation has preconditions: ",+                      TermPart req],+           SubReport [TextPart "States here are: ",+                      TermPart got]]+    renderPost : TT -> TT -> List (ErrorReportPart)+    renderPost got req +        = [SubReport [TextPart "Operation has postconditions: ",+                      TermPart req],+           SubReport [TextPart "Required result states here are: ",+                      TermPart got]]++st_precondition _ = Nothing

@@ -0,0 +1,13 @@+module Control.ST.ImplicitCall++import Control.ST++||| Make 'call' implicit.+||| This makes ST programs less verbose, at the cost of making error messages+||| potentially more difficult to read.+export implicit+imp_call : STrans m t ys ys' ->+       {auto ctxt_prf : SubCtxt ys xs} ->+       STrans m t xs (\res => updateWith (ys' res) xs ctxt_prf)+imp_call = call+

@@ -0,0 +1,160 @@+||| A Zipper implementation for Lists+||| inspired by+||| https://hackage.haskell.org/package/ListZipper-1.2.0.2/docs/src/Data-List-Zipper.html+module Data.List.Zipper++%default total+%access public export++||| A Zipper for Lists+data Zipper: Type -> Type where+  Zip: List a -> List a -> Zipper a++%name Zipper z1, z2++-- Implementations+--------------------------------------------------------------------------------++Functor Zipper where+  map f (Zip xs ys) = Zip (map f xs) (map f ys)++Foldable Zipper where+  foldr f acc (Zip xs ys) = foldr f acc (reverse xs ++ ys)++Show a => Show (Zipper a) where+  show (Zip xs []) = show $ reverse xs+  show (Zip xs (x :: ys)) = unwords [show $ reverse xs, "-", show x, "-", show ys]++||| Equality for Zippers+||| Two zipper are equal if they zip the same list and point to the same cursor+Eq a => Eq (Zipper a) where+  (==) (Zip xs ys) (Zip zs ws) = (xs == zs) && (ys == ws)+-- Functions+--------------------------------------------------------------------------------++||| creates an empty Zipper+||| ```idris example+||| empty {a = Nat}+||| ```+empty: Zipper a+empty = Zip [] []++||| checks whether this Zipper is empty+||| ```idris example+||| isEmpty empty {a = Nat}+||| ```+isEmpty: Zipper a -> Bool+isEmpty (Zip [] []) = True+isEmpty _ = False++||| creates a Zipper from a List+||| ```idris example+||| show $ fromList [1,2,3,4,5]+||| ```+fromList: List a -> Zipper a+fromList xs = Zip [] xs++||| moves the cursor to the right or leaves the cursor unchanged+||| ```idris example+|||  show $ right $ fromList [1,2,3,4,5]+||| ```+right: Zipper a -> Zipper a+right (Zip xs (x :: ys)) = Zip (x :: xs) ys+right z = z++||| moves the cursor to the left or leaves the cursor unchanged+||| ```idris example+||| show $ left $ fromList [1,2,3,4,5]+||| ```+left: Zipper a -> Zipper a+left (Zip (x :: xs) ys) = Zip xs (x :: ys)+left z = z++||| gets the element at the current cursor+||| ```idris example+||| cursor $ fromList [1,2,3,4,5]+||| ```+cursor: Zipper a -> Maybe a+cursor (Zip xs ys) = listToMaybe ys++||| move the cursor to the start of the Zipper+||| ```idris example+||| show $ start $ fromList [1,2,3,4,5]+||| ```+start: Zipper a -> Zipper a+start (Zip xs ys) = Zip [] (reverse xs ++ ys)++||| move the cursor to the end of the Zipper+||| ```idris example+||| show $ end $ fromList [1,2,3,4,5]+||| ```+end: Zipper a -> Zipper a+end (Zip xs ys) = Zip (reverse ys ++ xs) []++||| checks whether the cursor is at the start of the Zipper+||| ```idris example+||| startp $ fromList [1,2,3,4,5]+||| ```+startp: Zipper a -> Bool+startp (Zip [] ys) = True+startp _ = False++||| checks whether the cursor is at the end of the Zipper+||| ```idris example+||| endp $ fromList [1,2,3,4,5]+||| ```+endp: Zipper a -> Bool+endp (Zip xs []) = True+endp _ = False++||| inserts an element at the current cursor+||| ```idris example+||| show $ insert 0 $ fromList [1,2,3,4,5]+||| ```+insert: a -> Zipper a -> Zipper a+insert x (Zip xs ys) = Zip xs (x :: ys)++||| push an element into the Zipper and move the cursor past it+||| ```idris example+||| show $ push 0 $ fromList [1,2,3,4,5]+||| ```+push: a -> Zipper a -> Zipper a+push x (Zip xs ys) = Zip (x :: xs) (ys)++||| pop an element from the Zipper+||| ```idris example+||| show $ pop $ right $ fromList [1,2,3,4,5]+||| ```+pop: Zipper a -> Zipper a+pop (Zip (_ :: xs) ys) = Zip xs ys+pop z = z++||| delete the element at the current cursor+||| ```idris example+||| show $ Data.List.Zipper.delete $ fromList [1,2,3,4,5]+||| ```+delete: Zipper a -> Zipper a+delete (Zip xs (x :: ys)) = Zip xs ys+delete z = z++||| remove an element from the zipper+||| ```idris example+||| show $ replace 9 $ fromList[1,2,3,4,5]+||| ```+replace: a -> Zipper a -> Zipper a+replace x (Zip xs (_ :: ys)) = Zip xs (x :: ys)+replace _ z1 = z1++||| Return the index of the current cursor+||| ```idris example+||| index $ fromList [1,2,3,4,5]+||| ```+index: Zipper a -> Nat+index (Zip xs ys) = length xs++||| convert this Zipper to a list+||| ```idris example+||| toList $ fromList[1,2,3,4,5]+||| ```+toList: Zipper a -> List a+toList (Zip xs ys) = reverse xs ++ ys

@@ -0,0 +1,33 @@+||| Ported from Haskell:+||| https://hackage.haskell.org/package/base-4.9.0.0/docs/src/Data.Monoid.html+module Data.Monoid++%access public export+%default total++-- TODO: These instances exist, but can't be named the same.+-- Decide on names for these++-- [all] Semigroup Bool where+--   a <+> b = a && b+--+-- [all] Monoid Bool where+--   neutral = True+--+-- [any] Semigroup Bool where+--   a <+> b = a || b+--+-- [any] Monoid Bool where+--   neutral = False++Semigroup () where+  (<+>) _ _ = ()++Monoid () where+  neutral = ()++(Semigroup m, Semigroup n) => Semigroup (m, n) where+  (a, b) <+> (c, d) = (a <+> c, b <+> d)++(Monoid m, Monoid n) => Monoid (m, n) where+  neutral = (neutral, neutral)

@@ -6,7 +6,6 @@ %default total %access public export - ||| An integer is either a positive `Nat` or the negated successor of a `Nat`. ||| ||| For example, 3 is `Pos 3` and -2 is `NegS 1`. Zero is arbitrarily chosen@@ -51,7 +50,6 @@   (NegS n) == (NegS m) = n == m   _ == _ = False - implementation Ord ZZ where   compare (Pos n) (Pos m) = compare n m   compare (NegS n) (NegS m) = compare m n@@ -84,7 +82,7 @@     negate (Pos Z)     = Pos Z     negate (Pos (S n)) = NegS n     negate (NegS n)    = Pos (S n)-  +     (-) = subZ     abs = cast . absZ @@ -92,7 +90,6 @@   subZ : ZZ -> ZZ -> ZZ   subZ n m = plusZ n (negate m) - implementation Cast ZZ Integer where   cast (Pos n) = cast n   cast (NegS n) = (-1) * (cast n + 1)@@ -100,7 +97,6 @@ implementation Cast Integer ZZ where   cast = fromInteger - -------------------------------------------------------------------------------- -- Properties --------------------------------------------------------------------------------@@ -141,6 +137,7 @@     | No p = No $ \h => p $ negSInjective h  -- Plus+ plusZeroLeftNeutralZ : (right : ZZ) -> 0 + right = right plusZeroLeftNeutralZ (Pos n) = Refl plusZeroLeftNeutralZ (NegS n) = Refl@@ -155,3 +152,202 @@ plusCommutativeZ (NegS n) (Pos m) = Refl plusCommutativeZ (NegS n) (NegS m) = cong {f=NegS} $ cong {f=S} $ plusCommutative n m +minusNatZAntiCommutative : (j, k : Nat) -> negate (minusNatZ j k) = minusNatZ k j+minusNatZAntiCommutative Z Z = Refl+minusNatZAntiCommutative Z (S k) = Refl+minusNatZAntiCommutative (S j) Z = Refl+minusNatZAntiCommutative (S j) (S k) = minusNatZAntiCommutative j k++negateDistributesPlus : (a, b : ZZ) -> negate (a + b) = (negate a) + (negate b)+negateDistributesPlus (Pos Z) b = rewrite plusZeroLeftNeutralZ b in+                                  rewrite plusZeroLeftNeutralZ (negate b) in Refl+negateDistributesPlus (Pos (S k)) (Pos Z) = rewrite plusZeroRightNeutral k in Refl+negateDistributesPlus (Pos (S k)) (Pos (S j)) = rewrite plusCommutative k (S j) in+                                                rewrite plusCommutative j k in Refl+negateDistributesPlus (Pos (S k)) (NegS j) = minusNatZAntiCommutative k j+negateDistributesPlus (NegS k) (Pos Z) = rewrite plusZeroRightNeutral k in Refl+negateDistributesPlus (NegS k) (Pos (S j)) = minusNatZAntiCommutative j k+negateDistributesPlus (NegS k) (NegS j) = rewrite plusCommutative k (S j) in+                                          rewrite plusCommutative k j in Refl++lemmaMinusSucc : (k, j, i : Nat) -> plusZ (minusNatZ k (S j)) (Pos i) = plusZ (minusNatZ k (S (S j))) (Pos (S i))+lemmaMinusSucc Z j i = Refl+lemmaMinusSucc (S Z) Z i = Refl+lemmaMinusSucc (S (S k)) Z i = rewrite plusCommutative k (S i) in+                               rewrite plusCommutative i k in Refl+lemmaMinusSucc (S k) (S j) i = lemmaMinusSucc k j i++lemmaAssocNegation : (k : Nat) -> (c, r : ZZ) -> (Pos (S k)) + (c + r) = ((Pos (S k)) + c) + r -> (NegS k) + ((negate c) + (negate r)) = ((NegS k) + (negate c)) + (negate r)+lemmaAssocNegation k c r prf = rewrite sym $ negateDistributesPlus c r in+                               rewrite sym $ negateDistributesPlus (Pos (S k)) (plusZ c r) in+                               rewrite sym $ negateDistributesPlus (Pos (S k)) c in+                               rewrite sym $ negateDistributesPlus (plusZ (Pos (S k)) c) r in+                               cong $ prf++lemmaAssocPos : (k : Nat) -> (c, r : ZZ) -> (Pos k) + (c + r) = ((Pos k) + c) + r+lemmaAssocPos k (Pos j) (Pos i) = cong $ plusAssociative k j i+lemmaAssocPos k (Pos Z) (NegS i) = rewrite plusZeroRightNeutral k in Refl+lemmaAssocPos k (Pos (S j)) (NegS Z) = rewrite plusCommutative k (S j) in+                                       rewrite plusCommutative j k in Refl+lemmaAssocPos k (Pos (S j)) (NegS (S i)) = let ind = lemmaAssocPos k (assert_smaller (Pos (S j)) (Pos j)) (assert_smaller (NegS (S i)) (NegS i)) in+                                           rewrite ind in+                                           rewrite plusCommutative k (S j) in+                                           rewrite plusCommutative j k in Refl+lemmaAssocPos k (NegS j) (Pos Z) = rewrite plusZeroRightNeutralZ (minusNatZ k (S j)) in Refl+lemmaAssocPos Z (NegS Z) (Pos (S i)) = Refl+lemmaAssocPos (S k) (NegS Z) (Pos (S i)) = rewrite plusCommutative k (S i) in+                                           rewrite plusCommutative k i in Refl+lemmaAssocPos k (NegS (S j)) (Pos (S i)) = let ind = lemmaAssocPos k (assert_smaller (NegS (S j)) (NegS j)) (assert_smaller (Pos (S i)) (Pos i)) in+                                           rewrite ind in+                                           rewrite lemmaMinusSucc k j i in Refl+lemmaAssocPos Z (NegS j) (NegS i) = Refl+lemmaAssocPos (S k) (NegS Z) (NegS i) = Refl+lemmaAssocPos (S k) (NegS (S j)) (NegS i) = let ind = lemmaAssocPos (assert_smaller (S k) k) (assert_smaller (NegS (S j)) (NegS j)) (NegS i) in+                                            rewrite ind in Refl++plusAssociativeZ : (l, c, r : ZZ) -> l + (c + r) = (l + c) + r+plusAssociativeZ (Pos k) c r = lemmaAssocPos k c r+plusAssociativeZ (NegS k) c r = rewrite sym $ doubleNegElim c in+                                rewrite sym $ doubleNegElim r in+                                lemmaAssocNegation k (negate c) (negate r) (lemmaAssocPos (S k) (negate c) (negate r))++lemmaMinusSymmZero : (k : Nat) -> minusNatZ k k = Pos 0+lemmaMinusSymmZero Z = Refl+lemmaMinusSymmZero (S k) = let ind = lemmaMinusSymmZero k in+                           rewrite ind in Refl++plusNegateInverseLZ : (a : ZZ) -> a + negate a = Pos Z+plusNegateInverseLZ (Pos Z) = Refl+plusNegateInverseLZ (Pos (S k)) = rewrite lemmaMinusSymmZero k in Refl+plusNegateInverseLZ (NegS k) = rewrite lemmaMinusSymmZero k in Refl++plusNegateInverseRZ : (a : ZZ) -> negate a + a = Pos Z+plusNegateInverseRZ (Pos Z) = Refl+plusNegateInverseRZ (Pos (S k)) = rewrite lemmaMinusSymmZero k in Refl+plusNegateInverseRZ (NegS k) = rewrite lemmaMinusSymmZero k in Refl++-- Mult+multZeroLeftZeroZ : (right : ZZ) -> (Pos Z) * right = (Pos Z)+multZeroLeftZeroZ (Pos k) = Refl+multZeroLeftZeroZ (NegS k) = Refl++multZeroRightZeroZ : (left : ZZ) -> left * (Pos Z) = (Pos Z)+multZeroRightZeroZ (Pos k) = rewrite multZeroRightZero k in Refl+multZeroRightZeroZ (NegS k) = rewrite multZeroRightZero k in Refl++multOneLeftNeutralZ : (right : ZZ) -> 1 * right = right+multOneLeftNeutralZ (Pos k) = rewrite plusZeroRightNeutral k in Refl+multOneLeftNeutralZ (NegS k) = rewrite plusZeroRightNeutral k in Refl++multOneRightNeutralZ : (left : ZZ) -> left * 1 = left+multOneRightNeutralZ (Pos Z) = Refl+multOneRightNeutralZ (Pos (S k)) = cong $ multOneRightNeutral (S k)+multOneRightNeutralZ (NegS k) = cong $ multOneRightNeutral k++multCommutativeZ : (left : ZZ) -> (right : ZZ) -> (left * right = right * left)+multCommutativeZ (Pos k) (Pos j) = cong $ multCommutative k j+multCommutativeZ (Pos k) (NegS j) = rewrite multCommutative j k in+                                    cong $ multRightSuccPlus k j+multCommutativeZ (NegS k) (Pos j) = rewrite multCommutative j (S k) in Refl+multCommutativeZ (NegS k) (NegS j) = cong $ multCommutative (S k) (S j)++lemmaPosMultNegNat : (k, j : Nat) -> multZ (Pos k) (negNat j) = negNat (mult k j)+lemmaPosMultNegNat k Z = rewrite multZeroRightZero k in Refl+lemmaPosMultNegNat k (S j) = Refl++lemmaNegMultNegNat : (k, j : Nat) -> multZ (NegS k) (negNat j) = multZ (Pos (S k)) (Pos j)+lemmaNegMultNegNat k Z = rewrite multZeroRightZero k in Refl+lemmaNegMultNegNat k (S j) = Refl++lemmaNegatePosNegNat : (k : Nat) -> negate (Pos k) = negNat k+lemmaNegatePosNegNat Z = Refl+lemmaNegatePosNegNat (S k) = Refl++multNegLeftZ : (k : Nat) -> (j : ZZ) -> (NegS k) * j = negate (Pos (S k) * j)+multNegLeftZ k (Pos j) = rewrite lemmaNegatePosNegNat ((S k) * j) in Refl+multNegLeftZ k (NegS j) = Refl++multNegateLeftZ : (k, j : ZZ) -> (negate k) * j = negate (k * j)+multNegateLeftZ (Pos Z) j = rewrite multZeroLeftZeroZ j in Refl+multNegateLeftZ (Pos (S k)) (Pos j) = rewrite lemmaNegatePosNegNat ((S k) * j) in Refl+multNegateLeftZ (Pos (S k)) (NegS j) = Refl+multNegateLeftZ (NegS k) j = rewrite sym $ doubleNegElim (multZ (Pos (S k)) j) in+                             rewrite multNegLeftZ k j in Refl++multAssociativeZPos : (k : Nat) -> (c, r : ZZ) -> (Pos k) * (c * r) = ((Pos k) * c) * r+multAssociativeZPos k (Pos j) (Pos i) = cong $ multAssociative k j i+multAssociativeZPos k (Pos j) (NegS i) = rewrite sym $ multAssociative k j (S i) in lemmaPosMultNegNat k (mult j (S i))+multAssociativeZPos k (NegS j) (Pos i) = rewrite multCommutative j i in+                                         rewrite sym $ multRightSuccPlus i j in+                                         rewrite lemmaPosMultNegNat k (mult i (S j)) in+                                         rewrite multCommutativeZ (negNat (mult k (S j))) (Pos i) in+                                         rewrite lemmaPosMultNegNat i (mult k (S j)) in+                                         rewrite multAssociative k i (S j) in+                                         rewrite multAssociative i k (S j) in+                                         rewrite multCommutative i k in Refl+multAssociativeZPos k (NegS j) (NegS i) = rewrite multCommutativeZ (negNat (mult k (S j))) (NegS i) in+                                          rewrite lemmaNegMultNegNat i (mult k (S j)) in+                                          rewrite multAssociative k (S j) (S i) in+                                          rewrite multCommutative (mult k (S j)) (S i) in Refl++multAssociativeZ : (l, c, r : ZZ) -> l * (c * r) = (l * c) * r+multAssociativeZ (Pos k) c r = multAssociativeZPos k c r+multAssociativeZ (NegS k) c r = rewrite multNegLeftZ k (c * r) in+                                rewrite multNegLeftZ k c in+                                rewrite multNegateLeftZ (multZ (Pos (S k)) c) r in+                                cong $ multAssociativeZPos (S k) c r++lemmaPlusPosNegCancel : (k, j, i : Nat) -> plusZ (Pos (plus k j)) (negNat (plus k i)) = plusZ (Pos j) (negNat i)+lemmaPlusPosNegCancel Z j i = Refl+lemmaPlusPosNegCancel (S Z) j Z = rewrite plusZeroRightNeutral j in Refl+lemmaPlusPosNegCancel (S Z) j (S i) = Refl+lemmaPlusPosNegCancel (S (S k)) j i = lemmaPlusPosNegCancel (S k) j i++lemmaPlusPosNegZero : (k : Nat) -> plusZ (Pos k) (negNat k) = Pos Z+lemmaPlusPosNegZero Z = Refl+lemmaPlusPosNegZero (S k) = rewrite lemmaMinusSymmZero k in Refl++negNatDistributesPlus : (j, k : Nat) -> plusZ (negNat j) (negNat k) = negNat (plus j k)+negNatDistributesPlus Z k = rewrite plusZeroLeftNeutralZ (negNat k) in Refl+negNatDistributesPlus (S j) Z = rewrite plusZeroRightNeutral j in Refl+negNatDistributesPlus (S j) (S k) = rewrite plusSuccRightSucc j k in Refl++-- Distributivity++multDistributesOverPlusRightPosPosZ : (l, c : Nat) -> (r : ZZ) -> (Pos l) * ((Pos c) + r) = ((Pos l) * (Pos c)) + ((Pos l) * r)+multDistributesOverPlusRightPosPosZ l c (Pos i) = rewrite multDistributesOverPlusRight l c i in Refl+multDistributesOverPlusRightPosPosZ l Z (NegS i) = rewrite multZeroRightZero l in+                                                   rewrite plusZeroLeftNeutralZ (negNat (mult l (S i))) in Refl+multDistributesOverPlusRightPosPosZ l (S c) (NegS Z) = rewrite multOneRightNeutral l in+                                                       rewrite multRightSuccPlus l c in+                                                       rewrite sym $ plusAssociativeZ (Pos l) (Pos (mult l c)) (negNat l) in+                                                       rewrite plusCommutativeZ (Pos (mult l c)) (negNat l) in+                                                       rewrite plusAssociativeZ (Pos l) (negNat l) (Pos (mult l c)) in+                                                       rewrite lemmaPlusPosNegZero l in Refl+multDistributesOverPlusRightPosPosZ l (S c) (NegS (S i)) = let ind = multDistributesOverPlusRightPosPosZ l (assert_smaller (S c) c) (assert_smaller (NegS (S i)) (NegS i)) in+                                                           rewrite ind in+                                                           rewrite multRightSuccPlus l (S i) in+                                                           rewrite multRightSuccPlus l c in+                                                           rewrite lemmaPlusPosNegCancel l (mult l c) (mult l (S i)) in Refl++multDistributesOverPlusRightPosZ : (k : Nat) -> (c, r : ZZ) -> (Pos k) * (c + r) = ((Pos k) * c) + ((Pos k) * r)+multDistributesOverPlusRightPosZ k (Pos j) r = multDistributesOverPlusRightPosPosZ k j r+multDistributesOverPlusRightPosZ k (NegS j) (Pos i) = rewrite plusCommutativeZ ((Pos k) * (NegS j)) ((Pos k) * (Pos i)) in+                                                      rewrite multDistributesOverPlusRightPosPosZ k i (NegS j) in Refl+multDistributesOverPlusRightPosZ k (NegS j) (NegS i) = rewrite negNatDistributesPlus (mult k (S j)) (mult k (S i)) in+                                                       rewrite sym $ multDistributesOverPlusRight k (S j) (S i) in+                                                       rewrite plusSuccRightSucc j i in Refl++multDistributesOverPlusRightZ : (l, c, r : ZZ) -> l * (c + r) = (l * c) + (l * r)+multDistributesOverPlusRightZ (Pos k) c r = multDistributesOverPlusRightPosZ k c r+multDistributesOverPlusRightZ (NegS k) c r = rewrite multNegLeftZ k (plusZ c r) in+                                             rewrite multNegLeftZ k c in+                                             rewrite multNegLeftZ k r in+                                             rewrite sym $ negateDistributesPlus (multZ (Pos (S k)) c) (multZ (Pos (S k)) r) in+                                             rewrite multDistributesOverPlusRightPosZ (S k) c r in Refl++multDistributesOverPlusLeftZ : (l, c, r : ZZ) -> (l + c) * r = (l * r) + (c * r)+multDistributesOverPlusLeftZ l c r = rewrite multCommutativeZ (l + c) r in+                                     rewrite multDistributesOverPlusRightZ r l c in+                                     rewrite multCommutativeZ r l in+                                     rewrite multCommutativeZ r c in Refl

@@ -36,7 +36,7 @@                                  mx >>= \x =>                                         pure (f x)   monadLeftIdentity : (x : a) -> (f : a -> m b) -> pure x >>= f = f x-  monadRightIdentity : (mx : m a) -> mx >>= pure = mx+  monadRightIdentity : (mx : m a) -> mx >>= Applicative.pure = mx   monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->                        (mx >>= f) >>= g = mx >>= (\x => f x >>= g) 

@@ -4,210 +4,20 @@ ||| Modified (C) The Idris Community, 2015, 2016 module Network.Socket +import public Network.Socket.Data+import Network.Socket.Raw+ %include C "idris_net.h" %include C "sys/types.h" %include C "sys/socket.h" %include C "netdb.h" --- ------------------------------------------------------------ [ Type Aliases ]--public export-ByteLength : Type-ByteLength = Int--public export-ResultCode : Type-ResultCode = Int--||| Protocol Number.-|||-||| Generally good enough to just set it to 0.-public export-ProtocolNumber : Type-ProtocolNumber = Int--||| SocketError: Error thrown by a socket operation-public export-SocketError : Type-SocketError = Int--||| SocketDescriptor: Native C Socket Descriptor-public export-SocketDescriptor : Type-SocketDescriptor = Int--public export-Port : Type-Port = Int---- --------------------------------------------------------------- [ Constants ]--||| Backlog used within listen() call -- number of incoming calls-public export-BACKLOG : Int-BACKLOG = 20---- FIXME: This *must* be pulled in from C-public export-EAGAIN : Int-EAGAIN = 11---- -------------------------------------------------------------- [ Interfaces ]--export-interface ToCode a where-  toCode : a -> Int---- --------------------------------------------------------- [ Socket Families ]--||| Socket Families-|||-||| The ones that people might actually use. We're not going to need US-||| Government proprietary ones.-public export-data SocketFamily : Type where-  ||| Unspecified-  AF_UNSPEC : SocketFamily--  ||| IP / UDP etc. IPv4-  AF_INET : SocketFamily--  |||  IP / UDP etc. IPv6-  AF_INET6 : SocketFamily--export-Show SocketFamily where-  show AF_UNSPEC = "AF_UNSPEC"-  show AF_INET   = "AF_INET"-  show AF_INET6  = "AF_INET6"--export-ToCode SocketFamily where-  toCode AF_UNSPEC = 0-  toCode AF_INET   = 2-  toCode AF_INET6  = 10--getSocketFamily : Int -> Maybe SocketFamily-getSocketFamily i =-    Prelude.List.lookup i [ (0, AF_UNSPEC)-                          , (2, AF_INET)-                          , (10, AF_INET6)-                          ]---- ------------------------------------------------------------ [ Socket Types ]-||| Socket Types.-public export-data SocketType : Type where-  ||| Not a socket, used in certain operations-  NotASocket : SocketType--  ||| TCP-  Stream : SocketType--  ||| UDP-  Datagram : SocketType--  ||| Raw sockets-  RawSocket : SocketType--export-Show SocketType where-  show NotASocket = "Not a socket"-  show Stream     = "Stream"-  show Datagram   = "Datagram"-  show RawSocket  = "Raw"--export-ToCode SocketType where-  toCode NotASocket = 0-  toCode Stream     = 1-  toCode Datagram   = 2-  toCode RawSocket  = 3---- ---------------------------------------------------------------- [ Pointers ]--data RecvStructPtr = RSPtr Ptr-data RecvfromStructPtr = RFPtr Ptr--export-data BufPtr = BPtr Ptr--export-data SockaddrPtr = SAPtr Ptr---- --------------------------------------------------------------- [ Addresses ]--||| Network Addresses-public export-data SocketAddress : Type where-  IPv4Addr : Int -> Int -> Int -> Int -> SocketAddress--  ||| Not implemented (yet)-  IPv6Addr : SocketAddress--  Hostname : String -> SocketAddress--  ||| Used when there's a parse error-  InvalidAddress : SocketAddress--export-Show SocketAddress where-  show (IPv4Addr i1 i2 i3 i4) = concat $ Prelude.List.intersperse "." (map show [i1, i2, i3, i4])-  show IPv6Addr               = "NOT IMPLEMENTED YET"-  show (Hostname host)        = host-  show InvalidAddress         = "Invalid"---- --------------------------------------------------------- [ UDP Information ]---- TODO: Expand to non-string payloads-export-record UDPRecvData where-  constructor MkUDPRecvData-  remote_addr : SocketAddress-  remote_port : Port-  recv_data   : String-  data_len    : Int--export-record UDPAddrInfo where-  constructor MkUDPAddrInfo-  remote_addr : SocketAddress-  remote_port : Port---- ---------------------------------------------------------- [ Socket Utilies ]--||| Frees a given pointer-export-sock_free : BufPtr -> IO ()-sock_free (BPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr--export-sockaddr_free : SockaddrPtr -> IO ()-sockaddr_free (SAPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr--||| Allocates an amount of memory given by the ByteLength parameter.-|||-||| Used to allocate a mutable pointer to be given to the Recv functions.-export-sock_alloc : ByteLength -> IO BufPtr-sock_alloc bl = map BPtr $ foreign FFI_C "idrnet_malloc" (Int -> IO Ptr) bl---- ----------------------------------------------------------------- [ Sockets ]-||| The metadata about a socket-export-record Socket where-  constructor MkSocket-  descriptor     : SocketDescriptor-  family         : SocketFamily-  socketType     : SocketType-  protocolNumber : ProtocolNumber-+%access export  -- ----------------------------------------------------- [ Network Socket API. ]  ||| Creates a UNIX socket with the given family, socket type and protocol ||| number. Returns either a socket or an error.-export socket : (fam  : SocketFamily)       -> (ty   : SocketType)       -> (pnum : ProtocolNumber)@@ -222,34 +32,30 @@     else pure $ Right (MkSocket socket_res sf st pn)  ||| Close a socket-export close : Socket -> IO () close sock = foreign FFI_C "close" (Int -> IO ()) (descriptor sock) -private-saString : (Maybe SocketAddress) -> String-saString (Just sa) = show sa-saString Nothing = ""- ||| Binds a socket to the given socket address and port. ||| Returns 0 on success, an error code otherwise.-export bind : (sock : Socket)     -> (addr : Maybe SocketAddress)     -> (port : Port)     -> IO Int bind sock addr port = do-  bind_res <- foreign FFI_C "idrnet_bind"-                  (Int -> Int -> Int -> String -> Int -> IO Int)-                  (descriptor sock) (toCode $ family sock)-                  (toCode $ socketType sock) (saString addr) port-  if bind_res == (-1)-    then getErrno-    else pure 0+    bind_res <- foreign FFI_C "idrnet_bind"+                    (Int -> Int -> Int -> String -> Int -> IO Int)+                    (descriptor sock) (toCode $ family sock)+                    (toCode $ socketType sock) (saString addr) port+    if bind_res == (-1)+      then getErrno+      else pure 0+  where+    saString : Maybe SocketAddress -> String+    saString (Just sa) = show sa+    saString Nothing   = ""  ||| Connects to a given address and port. ||| Returns 0 on success, and an error number on error.-export connect : (sock : Socket)        -> (addr : SocketAddress)        -> (port : Port)@@ -266,7 +72,6 @@ ||| Listens on a bound socket. ||| ||| @sock The socket to listen on.-export listen : (sock : Socket) -> IO Int listen sock = do   listen_res <- foreign FFI_C "listen" (Int -> Int -> IO Int)@@ -275,40 +80,6 @@     then getErrno     else pure 0 -||| Parses a textual representation of an IPv4 address into a SocketAddress-parseIPv4 : String -> SocketAddress-parseIPv4 str =-    case splitted of-      (i1 :: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4-      otherwise                   => InvalidAddress-  where-    toInt' : String -> Integer-    toInt' = cast--    toInt : String -> Int-    toInt s = fromInteger $ toInt' s--    splitted : List Int-    splitted = map toInt (Prelude.Strings.split (\c => c == '.') str)--||| Retrieves a socket address from a sockaddr pointer-getSockAddr : SockaddrPtr -> IO SocketAddress-getSockAddr (SAPtr ptr) = do-  addr_family_int <- foreign FFI_C "idrnet_sockaddr_family"-                             (Ptr -> IO Int)-                             ptr--  -- ASSUMPTION: Foreign call returns a valid int-  assert_total (case getSocketFamily addr_family_int of-    Just AF_INET => do-      ipv4_addr <- foreign FFI_C "idrnet_sockaddr_ipv4"-                           (Ptr -> IO String)-                           ptr--      pure $ parseIPv4 ipv4_addr-    Just AF_INET6 => pure IPv6Addr-    Just AF_UNSPEC => pure InvalidAddress)- ||| Accept a connection on the provided socket. ||| ||| Returns on failure a `SocketError`@@ -317,7 +88,6 @@ ||| + `SocketAddress` :: The ||| ||| @sock The socket used to establish connection.-export accept : (sock : Socket)       -> IO (Either SocketError (Socket, SocketAddress)) accept sock = do@@ -346,7 +116,6 @@ ||| ||| @sock The socket on which to send the message. ||| @msg  The data to send.-export send : (sock : Socket)     -> (msg  : String)     -> IO (Either SocketError ResultCode)@@ -359,20 +128,6 @@     then map Left getErrno     else pure $ Right send_res -freeRecvStruct : RecvStructPtr -> IO ()-freeRecvStruct (RSPtr p) =-    foreign FFI_C "idrnet_free_recv_struct"-            (Ptr -> IO ())-            p--||| Utility to extract data.-freeRecvfromStruct : RecvfromStructPtr -> IO ()-freeRecvfromStruct (RFPtr p) =-    foreign FFI_C "idrnet_free_recvfrom_struct"-            (Ptr -> IO ())-            p-- ||| Receive data on the specified socket. ||| ||| Returns on failure a `SocketError`@@ -382,7 +137,6 @@ ||| ||| @sock The socket on which to receive the message. ||| @len  How much of the data to send.-export recv : (sock : Socket)     -> (len : ByteLength)     -> IO (Either SocketError (String, ResultCode))@@ -413,48 +167,6 @@            freeRecvStruct (RSPtr recv_struct_ptr)            pure $ Right (payload, recv_res) -||| Sends the data in a given memory location-|||-||| Returns on failure a `SocketError`-||| Returns on success the `ResultCode`-|||-||| @sock The socket on which to send the message.-||| @ptr  The location containing the data to send.-||| @len  How much of the data to send.-sendBuf : (sock : Socket)-       -> (ptr  : BufPtr)-       -> (len  : ByteLength)-       -> IO (Either SocketError ResultCode)-sendBuf sock (BPtr ptr) len = do-  send_res <- foreign FFI_C "idrnet_send_buf"-                      (Int -> Ptr -> Int -> IO Int)-                      (descriptor sock) ptr len--  if send_res == (-1)-   then map Left getErrno-   else pure $ Right send_res--||| Receive data from a given memory location.-|||-||| Returns on failure a `SocketError`-||| Returns on success the `ResultCode`-|||-||| @sock The socket on which to receive the message.-||| @ptr  The location containing the data to receive.-||| @len  How much of the data to receive.-recvBuf : (sock : Socket)-       -> (ptr  : BufPtr)-       -> (len  : ByteLength)-       -> IO (Either SocketError ResultCode)-recvBuf sock (BPtr ptr) len = do-  recv_res <- foreign FFI_C "idrnet_recv_buf"-                      (Int -> Ptr -> Int -> IO Int)-                      (descriptor sock) ptr len--  if (recv_res == (-1))-    then map Left getErrno-    else pure $ Right recv_res- ||| Send a message. ||| ||| Returns on failure a `SocketError`@@ -464,7 +176,6 @@ ||| @addr Address of the recipient. ||| @port The port on which to send the message. ||| @msg  The message to send.-export sendTo : (sock : Socket)       -> (addr : SocketAddress)       -> (port : Port)@@ -479,58 +190,6 @@     then map Left getErrno     else pure $ Right sendto_res -||| Send a message stored in some buffer.-|||-||| Returns on failure a `SocketError`-||| Returns on success the `ResultCode`-|||-||| @sock The socket on which to send the message.-||| @addr Address of the recipient.-||| @port The port on which to send the message.-||| @ptr  A Pointer to the buffer containing the message.-||| @len  The size of the message.-sendToBuf : (sock : Socket)-         -> (addr : SocketAddress)-         -> (port : Port)-         -> (ptr  : BufPtr)-         -> (len  : ByteLength)-         -> IO (Either SocketError ResultCode)-sendToBuf sock addr p (BPtr dat) len = do-  sendto_res <- foreign FFI_C "idrnet_sendto_buf"-                   (Int -> Ptr -> Int -> String -> Int -> Int -> IO Int)-                   (descriptor sock) dat len (show addr) p (toCode $ family sock)--  if sendto_res == (-1)-    then map Left getErrno-    else pure $ Right sendto_res--||| Utility function to get the payload of the sent message as a `String`.-foreignGetRecvfromPayload : RecvfromStructPtr -> IO String-foreignGetRecvfromPayload (RFPtr p) =-  foreign FFI_C "idrnet_get_recvfrom_payload"-                (Ptr -> IO String)-                p--||| Utility function to return senders socket address.-foreignGetRecvfromAddr : RecvfromStructPtr -> IO SocketAddress-foreignGetRecvfromAddr (RFPtr p) = do-  sockaddr_ptr <- map SAPtr $ foreign FFI_C "idrnet_get_recvfrom_sockaddr"-                                      (Ptr -> IO Ptr)-                                      p-  getSockAddr sockaddr_ptr--||| Utility function to return sender's IPV4 port.-foreignGetRecvfromPort : RecvfromStructPtr -> IO Port-foreignGetRecvfromPort (RFPtr p) = do-  sockaddr_ptr <- foreign FFI_C "idrnet_get_recvfrom_sockaddr"-                          (Ptr -> IO Ptr)-                          p-  port         <- foreign FFI_C "idrnet_sockaddr_ipv4_port"-                          (Ptr -> IO Int)-                          sockaddr_ptr-  pure port-- ||| Receive a message. ||| ||| Returns on failure a `SocketError`.@@ -542,7 +201,6 @@ ||| @sock The channel on which to receive. ||| @len  Size of the expected message. |||-export recvFrom : (sock : Socket)         -> (len  : ByteLength)         -> IO (Either SocketError (UDPAddrInfo, String, ResultCode))@@ -570,42 +228,3 @@           freeRecvfromStruct recv_ptr'           pure $ Right (MkUDPAddrInfo addr port, payload, result) -||| Receive a message placed on a 'known' buffer.-|||-||| Returns on failure a `SocketError`.-||| Returns on success a pair of-||| + `UDPAddrInfo` :: The address of the sender.-||| + `Int`         :: Result value from underlying function.-|||-||| @sock The channel on which to receive.-||| @ptr  Pointer to the buffer to place the message.-||| @len  Size of the expected message.-|||-recvFromBuf : (sock : Socket)-           -> (ptr  : BufPtr)-           -> (len  : ByteLength)-           -> IO (Either SocketError (UDPAddrInfo, ResultCode))-recvFromBuf sock (BPtr ptr) bl = do-  recv_ptr <- foreign FFI_C "idrnet_recvfrom_buf"-                      (Int -> Ptr -> Int -> IO Ptr)-                      (descriptor sock) ptr bl--  let recv_ptr' = RFPtr recv_ptr--  if !(nullPtr recv_ptr)-    then map Left getErrno-    else do-      result <- foreign FFI_C "idrnet_get_recvfrom_res"-                        (Ptr -> IO Int)-                        recv_ptr-      if result == -1-        then do-          freeRecvfromStruct recv_ptr'-          map Left getErrno-        else do-          port <- foreignGetRecvfromPort recv_ptr'-          addr <- foreignGetRecvfromAddr recv_ptr'-          freeRecvfromStruct recv_ptr'-          pure $ Right (MkUDPAddrInfo addr port, result + 1)---- --------------------------------------------------------------------- [ EOF ]

@@ -0,0 +1,172 @@+||| Low-Level C Sockets bindings for Idris. Used by higher-level, cleverer things.+||| Types used by Network.Socket.Raw and Network.Socket.+|||+||| Original (C) SimonJF, MIT Licensed, 2014+||| Modified (C) The Idris Community, 2015, 2016+module Network.Socket.Data++%access public export++-- ------------------------------------------------------------ [ Type Aliases ]++ByteLength : Type+ByteLength = Int++ResultCode : Type+ResultCode = Int++||| Protocol Number.+|||+||| Generally good enough to just set it to 0.+ProtocolNumber : Type+ProtocolNumber = Int++||| SocketError: Error thrown by a socket operation+SocketError : Type+SocketError = Int++||| SocketDescriptor: Native C Socket Descriptor+SocketDescriptor : Type+SocketDescriptor = Int++Port : Type+Port = Int++-- --------------------------------------------------------------- [ Constants ]++||| Backlog used within listen() call -- number of incoming calls+BACKLOG : Int+BACKLOG = 20++EAGAIN : Int+EAGAIN =+  -- I'm sorry+  -- maybe+  unsafePerformIO $ foreign FFI_C "idrnet_geteagain" (() -> IO Int) ()++-- -------------------------------------------------------------- [ Interfaces ]++interface ToCode a where+  toCode : a -> Int++-- --------------------------------------------------------- [ Socket Families ]++||| Socket Families+|||+||| The ones that people might actually use. We're not going to need US+||| Government proprietary ones.+data SocketFamily : Type where+  ||| Unspecified+  AF_UNSPEC : SocketFamily++  ||| IP / UDP etc. IPv4+  AF_INET : SocketFamily++  |||  IP / UDP etc. IPv6+  AF_INET6 : SocketFamily++Show SocketFamily where+  show AF_UNSPEC = "AF_UNSPEC"+  show AF_INET   = "AF_INET"+  show AF_INET6  = "AF_INET6"++ToCode SocketFamily where+  toCode AF_UNSPEC = 0+  toCode AF_INET   = 2+  toCode AF_INET6  = 10++getSocketFamily : Int -> Maybe SocketFamily+getSocketFamily i =+    Prelude.List.lookup i [ (0, AF_UNSPEC)+                          , (2, AF_INET)+                          , (10, AF_INET6)+                          ]++-- ------------------------------------------------------------ [ Socket Types ]++||| Socket Types.+data SocketType : Type where+  ||| Not a socket, used in certain operations+  NotASocket : SocketType++  ||| TCP+  Stream : SocketType++  ||| UDP+  Datagram : SocketType++  ||| Raw sockets+  RawSocket : SocketType++Show SocketType where+  show NotASocket = "Not a socket"+  show Stream     = "Stream"+  show Datagram   = "Datagram"+  show RawSocket  = "Raw"++ToCode SocketType where+  toCode NotASocket = 0+  toCode Stream     = 1+  toCode Datagram   = 2+  toCode RawSocket  = 3++-- --------------------------------------------------------------- [ Addresses ]++||| Network Addresses+data SocketAddress : Type where+  IPv4Addr : Int -> Int -> Int -> Int -> SocketAddress++  ||| Not implemented (yet)+  IPv6Addr : SocketAddress++  Hostname : String -> SocketAddress++  ||| Used when there's a parse error+  InvalidAddress : SocketAddress++Show SocketAddress where+  show (IPv4Addr i1 i2 i3 i4) = concat $ Prelude.List.intersperse "." (map show [i1, i2, i3, i4])+  show IPv6Addr               = "NOT IMPLEMENTED YET"+  show (Hostname host)        = host+  show InvalidAddress         = "Invalid"++||| Parses a textual representation of an IPv4 address into a SocketAddress+parseIPv4 : String -> SocketAddress+parseIPv4 str =+    case splitted of+      (i1 :: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4+      otherwise                   => InvalidAddress+  where+    toInt' : String -> Integer+    toInt' = cast++    toInt : String -> Int+    toInt s = fromInteger $ toInt' s++    splitted : List Int+    splitted = map toInt (Prelude.Strings.split (\c => c == '.') str)++-- --------------------------------------------------------- [ UDP Information ]++-- TODO: Expand to non-string payloads+record UDPRecvData where+  constructor MkUDPRecvData+  remote_addr : SocketAddress+  remote_port : Port+  recv_data   : String+  data_len    : Int++record UDPAddrInfo where+  constructor MkUDPAddrInfo+  remote_addr : SocketAddress+  remote_port : Port++-- ----------------------------------------------------------------- [ Sockets ]+||| The metadata about a socket+record Socket where+  constructor MkSocket+  descriptor     : SocketDescriptor+  family         : SocketFamily+  socketType     : SocketType+  protocolNumber : ProtocolNumber+

@@ -0,0 +1,202 @@+||| Low-Level C Sockets bindings for Idris. Used by higher-level, cleverer things.+||| Type-unsafe parts. Use Network.Socket for a safe variant.+|||+||| Original (C) SimonJF, MIT Licensed, 2014+||| Modified (C) The Idris Community, 2015, 2016+module Network.Socket.Raw++import public Network.Socket.Data++%include C "idris_net.h"+%include C "sys/types.h"+%include C "sys/socket.h"+%include C "netdb.h"++%access public export++-- ---------------------------------------------------------------- [ Pointers ]++data RecvStructPtr     = RSPtr Ptr+data RecvfromStructPtr = RFPtr Ptr++data BufPtr = BPtr Ptr++data SockaddrPtr = SAPtr Ptr++-- ---------------------------------------------------------- [ Socket Utilies ]++||| Frees a given pointer+sock_free : BufPtr -> IO ()+sock_free (BPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr++sockaddr_free : SockaddrPtr -> IO ()+sockaddr_free (SAPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr++||| Allocates an amount of memory given by the ByteLength parameter.+|||+||| Used to allocate a mutable pointer to be given to the Recv functions.+sock_alloc : ByteLength -> IO BufPtr+sock_alloc bl = map BPtr $ foreign FFI_C "idrnet_malloc" (Int -> IO Ptr) bl++||| Retrieves a socket address from a sockaddr pointer+getSockAddr : SockaddrPtr -> IO SocketAddress+getSockAddr (SAPtr ptr) = do+  addr_family_int <- foreign FFI_C "idrnet_sockaddr_family"+                             (Ptr -> IO Int)+                             ptr++  -- ASSUMPTION: Foreign call returns a valid int+  assert_total (case getSocketFamily addr_family_int of+    Just AF_INET => do+      ipv4_addr <- foreign FFI_C "idrnet_sockaddr_ipv4"+                           (Ptr -> IO String)+                           ptr++      pure $ parseIPv4 ipv4_addr+    Just AF_INET6 => pure IPv6Addr+    Just AF_UNSPEC => pure InvalidAddress)++freeRecvStruct : RecvStructPtr -> IO ()+freeRecvStruct (RSPtr p) =+    foreign FFI_C "idrnet_free_recv_struct"+            (Ptr -> IO ())+            p++||| Utility to extract data.+freeRecvfromStruct : RecvfromStructPtr -> IO ()+freeRecvfromStruct (RFPtr p) =+    foreign FFI_C "idrnet_free_recvfrom_struct"+            (Ptr -> IO ())+            p++||| Sends the data in a given memory location+|||+||| Returns on failure a `SocketError`+||| Returns on success the `ResultCode`+|||+||| @sock The socket on which to send the message.+||| @ptr  The location containing the data to send.+||| @len  How much of the data to send.+sendBuf : (sock : Socket)+       -> (ptr  : BufPtr)+       -> (len  : ByteLength)+       -> IO (Either SocketError ResultCode)+sendBuf sock (BPtr ptr) len = do+  send_res <- foreign FFI_C "idrnet_send_buf"+                      (Int -> Ptr -> Int -> IO Int)+                      (descriptor sock) ptr len++  if send_res == (-1)+   then map Left getErrno+   else pure $ Right send_res++||| Receive data from a given memory location.+|||+||| Returns on failure a `SocketError`+||| Returns on success the `ResultCode`+|||+||| @sock The socket on which to receive the message.+||| @ptr  The location containing the data to receive.+||| @len  How much of the data to receive.+recvBuf : (sock : Socket)+       -> (ptr  : BufPtr)+       -> (len  : ByteLength)+       -> IO (Either SocketError ResultCode)+recvBuf sock (BPtr ptr) len = do+  recv_res <- foreign FFI_C "idrnet_recv_buf"+                      (Int -> Ptr -> Int -> IO Int)+                      (descriptor sock) ptr len++  if (recv_res == (-1))+    then map Left getErrno+    else pure $ Right recv_res++||| Send a message stored in some buffer.+|||+||| Returns on failure a `SocketError`+||| Returns on success the `ResultCode`+|||+||| @sock The socket on which to send the message.+||| @addr Address of the recipient.+||| @port The port on which to send the message.+||| @ptr  A Pointer to the buffer containing the message.+||| @len  The size of the message.+sendToBuf : (sock : Socket)+         -> (addr : SocketAddress)+         -> (port : Port)+         -> (ptr  : BufPtr)+         -> (len  : ByteLength)+         -> IO (Either SocketError ResultCode)+sendToBuf sock addr p (BPtr dat) len = do+  sendto_res <- foreign FFI_C "idrnet_sendto_buf"+                   (Int -> Ptr -> Int -> String -> Int -> Int -> IO Int)+                   (descriptor sock) dat len (show addr) p (toCode $ family sock)++  if sendto_res == (-1)+    then map Left getErrno+    else pure $ Right sendto_res++||| Utility function to get the payload of the sent message as a `String`.+foreignGetRecvfromPayload : RecvfromStructPtr -> IO String+foreignGetRecvfromPayload (RFPtr p) =+  foreign FFI_C "idrnet_get_recvfrom_payload"+                (Ptr -> IO String)+                p++||| Utility function to return senders socket address.+foreignGetRecvfromAddr : RecvfromStructPtr -> IO SocketAddress+foreignGetRecvfromAddr (RFPtr p) = do+  sockaddr_ptr <- map SAPtr $ foreign FFI_C "idrnet_get_recvfrom_sockaddr"+                                      (Ptr -> IO Ptr)+                                      p+  getSockAddr sockaddr_ptr++||| Utility function to return sender's IPV4 port.+foreignGetRecvfromPort : RecvfromStructPtr -> IO Port+foreignGetRecvfromPort (RFPtr p) = do+  sockaddr_ptr <- foreign FFI_C "idrnet_get_recvfrom_sockaddr"+                          (Ptr -> IO Ptr)+                          p+  port         <- foreign FFI_C "idrnet_sockaddr_ipv4_port"+                          (Ptr -> IO Int)+                          sockaddr_ptr+  pure port++||| Receive a message placed on a 'known' buffer.+|||+||| Returns on failure a `SocketError`.+||| Returns on success a pair of+||| + `UDPAddrInfo` :: The address of the sender.+||| + `Int`         :: Result value from underlying function.+|||+||| @sock The channel on which to receive.+||| @ptr  Pointer to the buffer to place the message.+||| @len  Size of the expected message.+|||+recvFromBuf : (sock : Socket)+           -> (ptr  : BufPtr)+           -> (len  : ByteLength)+           -> IO (Either SocketError (UDPAddrInfo, ResultCode))+recvFromBuf sock (BPtr ptr) bl = do+  recv_ptr <- foreign FFI_C "idrnet_recvfrom_buf"+                      (Int -> Ptr -> Int -> IO Ptr)+                      (descriptor sock) ptr bl++  let recv_ptr' = RFPtr recv_ptr++  if !(nullPtr recv_ptr)+    then map Left getErrno+    else do+      result <- foreign FFI_C "idrnet_get_recvfrom_res"+                        (Ptr -> IO Int)+                        recv_ptr+      if result == -1+        then do+          freeRecvfromStruct recv_ptr'+          map Left getErrno+        else do+          port <- foreignGetRecvfromPort recv_ptr'+          addr <- foreignGetRecvfromAddr recv_ptr'+          freeRecvfromStruct recv_ptr'+          pure $ Right (MkUDPAddrInfo addr port, result + 1)+

@@ -1,6 +1,6 @@ package contrib -opts = "--nobasepkgs --total -i ../prelude -i ../base"+opts = "--nobasepkgs --partial-eval --total -i ../prelude -i ../base" modules = CFFI, CFFI.Types, CFFI.Memory,            Control.Algebra,@@ -8,6 +8,7 @@           Control.Algebra.NumericImplementations,           Control.Isomorphism.Primitives,           Control.Partial,+          Control.ST, Control.ST.ImplicitCall,            Interfaces.Verified, @@ -20,10 +21,11 @@           Data.Heap,           Data.SortedMap, Data.SortedSet,           Data.CoList, Data.Storable,+	  Data.List.Zipper,            Decidable.Decidable, Decidable.Order, -          Network.Cgi, Network.Socket,+          Network.Cgi, Network.Socket.Data, Network.Socket.Raw, Network.Socket,            System.Concurrency.Process, 

@@ -17,7 +17,7 @@  implementation Show a => Handler (Exception a) IO where      handle _ (Raise e) k = do printLn e-                               believe_me (exit 1)+                               (exit 1)  implementation Handler (Exception a) (IOExcept a) where      handle _ (Raise e) k = ioe_fail e@@ -30,4 +30,3 @@  raise : a -> Eff b [EXCEPTION a] raise err = call $ Raise err-

@@ -1,6 +1,6 @@ package effects -opts    = "--nobasepkgs --typeintype -i ../prelude -i ../base"+opts    = "--nobasepkgs --partial-eval --typeintype -i ../prelude -i ../base"  modules = Effects         , Effect.Default

@@ -2,6 +2,7 @@  %access public export %default total+%language UniquenessTypes  ||| The canonical single-element type, also known as the trivially ||| true proposition.@@ -176,6 +177,12 @@ ||| is unreachable assert_unreachable : a -- compiled as primitive++||| Abort immediately with an error message+idris_crash : (msg : String) -> a+-- compiled as primitive++%used idris_crash msg  ||| Subvert the type checker. This function is abstract, so it will not reduce in ||| the type checker. Use it with care - it can result in segfaults or worse!

@@ -37,6 +37,8 @@ %access public export %default total +%language ElabReflection+ -- Things that can't be elsewhere for import cycle reasons -- See comment after declaration of void in Builtins.idr -- for explanation of this definition's location@@ -144,9 +146,14 @@   where go Z = []         go (S n) = n :: go n + -- predefine Nat versions of Enum, so we can use them in the default impls+countFrom : Num n => n -> n -> Stream n+countFrom start diff = start :: countFrom (start + diff) diff+ total natEnumFromThen : Nat -> Nat -> Stream Nat-natEnumFromThen n next = n :: natEnumFromThen next (minus next n)+natEnumFromThen n next = countFrom n (minus next n)+ total natEnumFromTo : Nat -> Nat -> List Nat natEnumFromTo n m = if n <= m                     then go n m@@ -195,7 +202,7 @@   succ n = n + 1   toNat n = cast n   fromNat n = cast n-  enumFromThen n inc = n :: enumFromThen (inc + n) inc+  enumFromThen n inc = countFrom n (inc - n)   enumFromTo n m = if n <= m                    then go n m                    else List.reverse $ go m n@@ -224,7 +231,8 @@           go' acc (S k) m = go' (m :: acc) k (m - 1)           go : Int -> Int -> List Int           go n m = go' [] (cast {to = Nat} (m - n)) m-  enumFromThen n inc = n :: enumFromThen (inc + n) inc+  enumFromThen n inc = countFrom n (inc - n)+   enumFromThenTo n next m = if n == m then [n]                             else if next - n == 0 || next - n < 0 /= m - n < 0 then []                             else go (natRange (S (divNatNZ (cast {to=Nat} (abs (m - n))) (S (cast {to=Nat} ((abs (next - n)) - 1))) SIsNotZ)))

@@ -1,3 +1,8 @@+||| Functions operating over Chars.+|||+||| The representation of a Char is backend dependent,+||| for the C backend, it is a Unicode code point.+||| module Prelude.Chars -- Functions operating over Chars @@ -9,7 +14,7 @@  %access public export -||| Convert the number to its ASCII equivalent.+||| Convert the number to its backend dependent (usually Unicode) Char equivelent. chr : Int -> Char chr x = if (x >= 0 && x < 0x110000)                 then assert_total (prim__intToChar x)@@ -18,7 +23,7 @@ Cast Int Char where     cast = chr -||| Return the ASCII representation of the character.+||| Return the backend dependent (usually Unicode) numerical equivelent of the Char. ord : Char -> Int ord x = prim__charToInt x 

@@ -547,7 +547,8 @@ -- Filters -------------------------------------------------------------------------------- -||| filter, applied to a predicate and a list, returns the list of those elements that satisfy the predicate; e.g.,+||| filter, applied to a predicate and a list, returns the list of those+||| elements that satisfy the predicate; e.g., ||| ||| ````idris example ||| filter (< 3) [Z, S Z, S (S Z), S (S (S Z)), S (S (S (S Z)))]@@ -569,7 +570,8 @@   filterSmaller {p = p} (x :: xs) | True = LTESucc (filterSmaller xs)  -||| The nubBy function behaves just like nub, except it uses a user-supplied equality predicate instead of the overloaded == function.+||| The nubBy function behaves just like nub, except it uses a user-supplied+||| equality predicate instead of the overloaded == function. nubBy : (a -> a -> Bool) -> List a -> List a nubBy = nubBy' []   where@@ -680,7 +682,9 @@ splitAt : (n : Nat) -> (xs : List a) -> (List a, List a) splitAt n xs = (take n xs, drop n xs) -||| 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; e.g.,+||| 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;+||| e.g., ||| ||| ```idris example ||| partition (<3) [0, 1, 2, 3, 4, 5]@@ -763,7 +767,8 @@ isSuffixOf : Eq a => List a -> List a -> Bool isSuffixOf = isSuffixOfBy (==) -||| The isInfixOf function takes two lists and returns True iff the first list is contained, wholly and intact, anywhere within the second.+||| The isInfixOf function takes two lists and returns True iff the first list+||| is contained, wholly and intact, anywhere within the second. ||| ||| ```idris example ||| isInfixOf ['b','c'] ['a', 'b', 'c', 'd']

@@ -91,6 +91,12 @@ -- Comparisons -------------------------------------------------------------------------------- +||| Proofs that `n` or `m` is not equal to Z+data NotBothZero : (n, m : Nat) -> Type where+  LeftIsNotZero  : NotBothZero (S n) m+  RightIsNotZero : NotBothZero n     (S m)++ ||| Proofs that `n` is less than or equal to `m` ||| @ n the smaller number ||| @ m the larger number@@ -386,16 +392,15 @@ -------------------------------------------------------------------------------- -- GCD and LCM ---------------------------------------------------------------------------------partial-gcd : Nat -> Nat -> Nat-gcd a Z = a-gcd a b = assert_total (gcd b (a `modNat` b))+gcd : (a: Nat) -> (b: Nat) -> .{auto ok: NotBothZero a b} -> Nat+gcd a Z     = a+gcd Z b     = b+gcd a (S b) = assert_total $ gcd (S b) (modNatNZ a (S b) SIsNotZ) -partial lcm : Nat -> Nat -> Nat-lcm _ Z = Z-lcm Z _ = Z-lcm x y = divNat (x * y) (gcd x y)+lcm _ Z     = Z+lcm Z _     = Z+lcm a (S b) = assert_total $ divNat (a * (S b)) (gcd a (S b))   --------------------------------------------------------------------------------

@@ -45,7 +45,8 @@ ||| ``` partial strHead : String -> Char-strHead = prim__strHead+strHead "" = idris_crash "Prelude.Strings: attempt to take the head of an empty string"+strHead x = prim__strHead x  ||| Returns the characters specified after the head of the string. |||@@ -59,7 +60,8 @@ ||| ``` partial strTail : String -> String-strTail = prim__strTail+strTail "" = idris_crash "Prelude.Strings: attempt to take the tail of an empty string"+strTail xs = prim__strTail xs  ||| Adds a character to the front of the specified string. |||@@ -72,6 +74,18 @@ strCons : Char -> String -> String strCons = prim__strCons +||| Returns the length of the string.+|||+||| ```idris example+||| length ""+||| ```+||| ```idris example+||| length "ABC"+||| ```+length : String -> Nat+length = fromInteger . prim__zextInt_BigInt . prim_lenString++ ||| Returns the nth character (starting from 0) of the specified string. ||| ||| Precondition: '0 < i < length s' for 'strIndex s i'.@@ -81,7 +95,9 @@ ||| ``` partial strIndex : String -> Int -> Char-strIndex = prim__strIndex+strIndex x i = if (i < 0 || i >= cast (length x))+                  then idris_crash "Prelude.Strings: String index out of bounds"+                  else prim__strIndex x i  ||| Reverses the elements within a String. |||@@ -296,17 +312,6 @@ ||| ``` unlines : List String -> String unlines = pack . unlines' . map unpack--||| Returns the length of the string.-|||-||| ```idris example-||| length ""-||| ```-||| ```idris example-||| length "ABC"-||| ```-length : String -> Nat-length = fromInteger . prim__zextInt_BigInt . prim_lenString  ||| Returns a substring of a given string |||

@@ -1,6 +1,6 @@ package prelude -opts = "--nobuiltins --total --no-elim-deprecation-warnings"+opts = "--nobuiltins --total --no-elim-deprecation-warnings --partial-eval" modules = Builtins, Prelude, IO,            Prelude.Algebra, Prelude.Basics, Prelude.Bool, Prelude.Cast,

@@ -132,7 +132,9 @@        (_, ty) <- check !getEnv subj        ty' <- forget ty        case headName ty' of-         Nothing => fail [TermPart ty, TextPart "is not an inductive family"]+         Nothing =>+           fail [TermPart ty,+                 TextPart "is not a datatype declared with the data keyword"]          Just fam =>            do let elim = elimN fam               (_,_,elimTy) <- (lookupTyExact elim) <|> (do deriveElim fam elim

@@ -1,6 +1,6 @@ package pruviloj -opts    = "--nobasepkgs -i ../prelude -i ../base"+opts    = "--nobasepkgs --partial-eval -i ../prelude -i ../base" modules = Pruviloj         , Pruviloj.Core         , Pruviloj.Derive.DecEq

@@ -1,10 +1,10 @@ module Main where -import System.Exit ( ExitCode(..), exitWith, exitSuccess )+import System.Exit (ExitCode(..), exitSuccess, exitWith) -import Control.Monad ( unless, when, (>=>) )-import Data.Maybe    ( fromMaybe )-import Data.Foldable ( foldrM )+import Control.Monad (unless, when, (>=>))+import Data.Foldable (foldrM)+import Data.Maybe (fromMaybe)  import Idris.AbsSyntax import Idris.CmdOptions@@ -15,8 +15,8 @@  import Util.System (setupBundledCC) -import Util.System ( setupBundledCC )-import System.Exit ( ExitCode(..), exitWith)+import System.Exit (ExitCode(..), exitWith)+import Util.System (setupBundledCC)  processShowOptions :: [Opt] -> Idris () processShowOptions opts = runIO $ do@@ -39,7 +39,7 @@ processClientOptions opts = check opts getClient $ \fs -> case fs of   []      -> ifail "No --client argument. This indicates a bug. Please report."   (c : _) -> do-    setVerbose False+    setVerbose 0     setQuiet True     case getPort opts of       Just  DontListen       -> ifail "\"--client\" and \"--port none\" are incompatible"

@@ -1,6 +1,6 @@ .\" Manpage for Idris. .\" Contact <> to correct errors or typos.-.TH man 1 "28 November 2016" "0.99" "Idris man page"+.TH man 1 "5 March 2017" "0.99.1" "Idris man page" .SH NAME idris -\ a general purpose pure functional programming language with dependent types. .SH SYNOPSIS@@ -68,7 +68,9 @@   --listlibs               Display installed libraries   --libdir                 Display library directory   --include                Display the includes flags-  -V,--verbose             Loud verbosity+  --V2                     Loudest verbosity+  --V1                     Louder verbosity+  -V, --V0, --verbose      Loud verbosity   --ibcsubdir FILE         Write IBC files into sub directory   -i,--idrispath ARG       Add directory to the list of import paths   --sourcepath ARG         Add directory to the list of source search paths@@ -91,8 +93,7 @@   --exec EXPR              Execute as idris   -X,--extension EXT       Turn on language extension (TypeProviders or                            ErrorReflection)-  --no-partial-eval        Switch off partial evaluation, mainly for debugging-                           purposes+  --partial-eval           Switch on partial evaluation   --target TRIPLE          If supported the codegen will target the named triple.   --cpu CPU                If supported the codegen will target the named CPU                            e.g. corei7 or cortex-m3.

@@ -1,4 +1,4 @@-#!/bin/sh+#!/usr/bin/env sh  set -euo pipefail @@ -62,3 +62,6 @@          --version "v$VERSION"       \          --root /tmp/idris-pkg/      \          idris-$VERSION.pkg++echo "==> Creating SHA256 hash (don't forget to update web site!)"+shasum -a 256 idris-$VERSION.pkg > idris-$VERSION.pkg.sha256

@@ -823,37 +823,37 @@ }  VAL idris_peekB8(VM* vm, VAL ptr, VAL offset) {-    return MKB8(vm, *(uint8_t*)(GETPTR(ptr) + GETINT(offset)));+    return MKB8(vm, *(uint8_t*)((char *)GETPTR(ptr) + GETINT(offset))); }  VAL idris_pokeB8(VAL ptr, VAL offset, VAL data) {-    *(uint8_t*)(GETPTR(ptr) + GETINT(offset)) = GETBITS8(data);+    *(uint8_t*)((char *)GETPTR(ptr) + GETINT(offset)) = GETBITS8(data);     return MKINT(0); }  VAL idris_peekB16(VM* vm, VAL ptr, VAL offset) {-    return MKB16(vm, *(uint16_t*)(GETPTR(ptr) + GETINT(offset)));+    return MKB16(vm, *(uint16_t*)((char *)GETPTR(ptr) + GETINT(offset))); }  VAL idris_pokeB16(VAL ptr, VAL offset, VAL data) {-    *(uint16_t*)(GETPTR(ptr) + GETINT(offset)) = GETBITS16(data);+    *(uint16_t*)((char *)GETPTR(ptr) + GETINT(offset)) = GETBITS16(data);     return MKINT(0); }  VAL idris_peekB32(VM* vm, VAL ptr, VAL offset) {-    return MKB32(vm, *(uint32_t*)(GETPTR(ptr) + GETINT(offset)));+    return MKB32(vm, *(uint32_t*)((char *)GETPTR(ptr) + GETINT(offset))); }  VAL idris_pokeB32(VAL ptr, VAL offset, VAL data) {-    *(uint32_t*)(GETPTR(ptr) + GETINT(offset)) = GETBITS32(data);+    *(uint32_t*)((char *)GETPTR(ptr) + GETINT(offset)) = GETBITS32(data);     return MKINT(0); }  VAL idris_peekB64(VM* vm, VAL ptr, VAL offset) {-    return MKB64(vm, *(uint64_t*)(GETPTR(ptr) + GETINT(offset)));+    return MKB64(vm, *(uint64_t*)((char *)GETPTR(ptr) + GETINT(offset))); }  VAL idris_pokeB64(VAL ptr, VAL offset, VAL data) {-    *(uint64_t*)(GETPTR(ptr) + GETINT(offset)) = GETBITS64(data);+    *(uint64_t*)((char *)GETPTR(ptr) + GETINT(offset)) = GETBITS64(data);     return MKINT(0); }

@@ -1,3 +1,4 @@+#include "idris_heap.h" #include "idris_rts.h" #include "idris_gc.h" #include "idris_bitstring.h"@@ -73,7 +74,7 @@ void cheney(VM *vm) {     int i;     int ar;-    char* scan = vm->heap.heap;+    char* scan = aligned_heap_pointer(vm->heap.heap);      while(scan < vm->heap.next) {        size_t inc = *((size_t*)scan);

@@ -14,7 +14,7 @@ // much space is needed (or find another way of preventing copying) #define IDRIS_MAXGMP 65536 -void init_gmpalloc() {+void init_gmpalloc(void) {     mp_set_memory_functions(idris_alloc, idris_realloc, idris_free); } 

@@ -8,7 +8,7 @@ #endif  // Set memory allocation functions-void init_gmpalloc();+void init_gmpalloc(void);  VAL MKBIGI(int val); VAL MKBIGC(VM* vm, char* bigint);

@@ -118,14 +118,7 @@     }      h->heap = mem;-#ifdef FORCE_ALIGNMENT-    if (((i_int)(h->heap)&1) == 1) {-        h->next = h->heap + 1;-    } else-#endif-    {-        h->next = h->heap;-    }+    h->next = aligned_heap_pointer(h->heap);     h->end  = h->heap + heap_size;      h->size   = heap_size;@@ -167,6 +160,17 @@  int ref_in_heap(Heap * heap, VAL v) {     return ((VAL)heap->heap <= v) && (v < (VAL)heap->next);+}++char* aligned_heap_pointer(char * heap) {+#ifdef FORCE_ALIGNMENT+    if (((i_int)heap&1) == 1) {+	    return (heap + 1);+    } else+#endif+    {+	    return heap;+    } }  // Checks three important properties:

@@ -98,7 +98,7 @@  void alloc_heap(Heap * heap, size_t heap_size, size_t growth, char * old); void free_heap(Heap * heap);-+char* aligned_heap_pointer(char * heap);  #ifdef IDRIS_DEBUG void heap_check_all(Heap * heap);

@@ -1,7 +1,32 @@+#include "idris_gmp.h" #include "idris_opts.h"-#include "idris_stats.h" #include "idris_rts.h"-#include "idris_gmp.h"+#include "idris_stats.h"++#if defined(WIN32) || defined(__WIN32) || defined(__WIN32__)+#include <Windows.h>+int win32_get_argv_utf8(int *argc_ptr, char ***argv_ptr)+{+    int argc;+    char **argv;+    wchar_t **argv_utf16 = CommandLineToArgvW(GetCommandLineW(), &argc);+    int i;+    int offset = (argc + 1) * sizeof(char *);+    int size = offset;+    for (i = 0; i < argc; i++) {+        size += WideCharToMultiByte(CP_UTF8, 0, argv_utf16[i], -1, 0, 0, 0, 0);+    }+    argv = (char **)malloc(size);+    for (i = 0; i < argc; i++) {+        argv[i] = (char *)argv + offset;+        offset += WideCharToMultiByte(CP_UTF8, 0, argv_utf16[i], -1, argv[i], size - offset, 0, 0);+    }+    *argc_ptr = argc;+    *argv_ptr = argv;+    return 0;+}+#endif+ // The default options should give satisfactory results under many circumstances. RTSOpts opts = {      .init_heap_size = 16384000,@@ -9,7 +34,14 @@     .show_summary   = 0 }; -int main(int argc, char* argv[]) {+#if defined(WIN32) || defined(__WIN32) || defined(__WIN32__)+int main() {+    int argc;+    char **argv;+    win32_get_argv_utf8(&argc, &argv);+#else+int main(int argc, char **argv) {+#endif     parse_shift_args(&opts, &argc, &argv);      __idris_argc = argc;

@@ -315,3 +315,8 @@         }     } }++int idrnet_geteagain() {+    return EAGAIN;+}+

@@ -73,5 +73,6 @@ int idrnet_getaddrinfo(struct addrinfo** address_res, char* host,      int port, int family, int socket_type); +int idrnet_geteagain();  #endif

@@ -99,7 +99,7 @@     return argc; } -void parse_shift_args(RTSOpts * opts, int * argc, char ** argv[]) {+void parse_shift_args(RTSOpts * opts, int * argc, char *** argv) {     size_t shift = parse_args(opts, (*argc) - 1, (*argv) + 1);      char *prg = (*argv)[0];

@@ -14,6 +14,6 @@  // Parse rts options and shift arguments such that rts options becomes invisible // for main program.-void parse_shift_args(RTSOpts * opts, int * argc, char ** argv[]);+void parse_shift_args(RTSOpts * opts, int * argc, char *** argv);  #endif

@@ -70,7 +70,7 @@     return vm; } -VM* idris_vm() {+VM* idris_vm(void) {     VM* vm = init_vm(4096000, 4096000, 1);     init_threadkeys();     init_threaddata(vm);@@ -95,12 +95,12 @@ }  #ifdef HAS_PTHREAD-void create_key() {+void create_key(void) {     pthread_key_create(&vm_key, (void*)free_key); } #endif -void init_threadkeys() {+void init_threadkeys(void) { #ifdef HAS_PTHREAD     static pthread_once_t key_once = PTHREAD_ONCE_INIT;     pthread_once(&key_once, create_key);@@ -113,7 +113,7 @@ #endif } -void init_signals() {+void init_signals(void) { #if (__linux__ || __APPLE__ || __FreeBSD__ || __DragonFly__)     signal(SIGPIPE, SIG_IGN); #endif@@ -173,7 +173,7 @@ #endif } -void idris_doneAlloc() {+void idris_doneAlloc(void) { #ifdef HAS_PTHREAD     VM* vm = pthread_getspecific(vm_key);     int lock = vm->processes > 0;@@ -191,7 +191,7 @@     Closure* cl = (Closure*) allocate(sizeof(Closure)+size, 0);     SETTY(cl, CT_RAWDATA);     cl->info.size = size;-    return (void*)cl+sizeof(Closure);+    return (void*)((char *)cl+sizeof(Closure)); }  void* idris_realloc(void* old, size_t old_size, size_t size) {@@ -449,36 +449,36 @@   VAL idris_peekPtr(VM* vm, VAL ptr, VAL offset) {-    void** addr = GETPTR(ptr) + GETINT(offset);+    void** addr = (void **)((char *)GETPTR(ptr) + GETINT(offset));     return MKPTR(vm, *addr); }  VAL idris_pokePtr(VAL ptr, VAL offset, VAL data) {-    void** addr = GETPTR(ptr) + GETINT(offset);+    void** addr = (void **)((char *)GETPTR(ptr) + GETINT(offset));     *addr = GETPTR(data);     return MKINT(0); }  VAL idris_peekDouble(VM* vm, VAL ptr, VAL offset) {-    return MKFLOAT(vm, *(double*)(GETPTR(ptr) + GETINT(offset)));+    return MKFLOAT(vm, *(double*)((char *)GETPTR(ptr) + GETINT(offset))); }  VAL idris_pokeDouble(VAL ptr, VAL offset, VAL data) {-    *(double*)(GETPTR(ptr) + GETINT(offset)) = GETFLOAT(data);+    *(double*)((char *)GETPTR(ptr) + GETINT(offset)) = GETFLOAT(data);     return MKINT(0); }  VAL idris_peekSingle(VM* vm, VAL ptr, VAL offset) {-    return MKFLOAT(vm, *(float*)(GETPTR(ptr) + GETINT(offset)));+    return MKFLOAT(vm, *(float*)((char *)GETPTR(ptr) + GETINT(offset))); }  VAL idris_pokeSingle(VAL ptr, VAL offset, VAL data) {-    *(float*)(GETPTR(ptr) + GETINT(offset)) = GETFLOAT(data);+    *(float*)((char *)GETPTR(ptr) + GETINT(offset)) = GETFLOAT(data);     return MKINT(0); }  void idris_memmove(void* dest, void* src, i_int dest_offset, i_int src_offset, i_int size) {-    memmove(dest + dest_offset, src + src_offset, size);+    memmove((char *)dest + dest_offset, (char *)src + src_offset, size); }  VAL idris_castIntStr(VM* vm, VAL i) {@@ -595,6 +595,11 @@     return ret; } +void idris_crash(char* msg) {+    fprintf(stderr, "%s\n", msg);+    exit(1);+}+ VAL idris_strHead(VM* vm, VAL str) {     return idris_strIndex(vm, str, 0); }@@ -1041,7 +1046,7 @@     free(msg); } -int idris_errno() {+int idris_errno(void) {     return errno; } @@ -1051,7 +1056,7 @@  VAL* nullary_cons; -void init_nullaries() {+void init_nullaries(void) {     int i;     VAL cl;     nullary_cons = malloc(256 * sizeof(VAL));@@ -1063,7 +1068,7 @@     } } -void free_nullaries() {+void free_nullaries(void) {     int i;     for(i = 0; i < 256; ++i) {         free(nullary_cons[i]);@@ -1074,7 +1079,7 @@ int __idris_argc; char **__idris_argv; -int idris_numArgs() {+int idris_numArgs(void) {     return __idris_argc; } @@ -1082,12 +1087,12 @@     return __idris_argv[i]; } -void idris_disableBuffering() {+void idris_disableBuffering(void) {   setvbuf(stdin, NULL, _IONBF, 0);   setvbuf(stdout, NULL, _IONBF, 0); } -void stackOverflow() {+void stackOverflow(void) {   fprintf(stderr, "Stack overflow");   exit(-1); }

@@ -161,11 +161,11 @@  // Create a new VM, set up everything with sensible defaults (use when // calling Idris from C)-VM* idris_vm();+VM* idris_vm(void); void close_vm(VM* vm);  // Set up key for thread-local data - called once from idris_main-void init_threadkeys();+void init_threadkeys(void);  // Functions all take a pointer to their VM, and previous stack base, // and return nothing.@@ -278,7 +278,7 @@ // may take a lock if other threads are running).  void idris_requireAlloc(size_t size);-void idris_doneAlloc();+void idris_doneAlloc(void);  // public interface to allocation (note that this may move other pointers // if allocating beyond the limits given by idris_requireAlloc!)@@ -299,14 +299,14 @@  #define NULL_CON(x) nullary_cons[x] -int idris_errno();+int idris_errno(void); char* idris_showerror(int err);  extern VAL* nullary_cons;-void init_nullaries();-void free_nullaries();+void init_nullaries(void);+void free_nullaries(void); -void init_signals();+void init_signals(void);  void* vmThread(VM* callvm, func f, VAL arg); void* idris_stopThread(VM* vm);@@ -364,6 +364,9 @@ VAL idris_peekSingle(VM* vm, VAL ptr, VAL offset); VAL idris_pokeSingle(VAL ptr, VAL offset, VAL data); +// Crash with a message (used for partial primitives)+void idris_crash(char* msg);+ // String primitives VAL idris_concat(VM* vm, VAL l, VAL r); VAL idris_strlt(VM* vm, VAL l, VAL r);@@ -391,16 +394,16 @@ extern int __idris_argc; extern char **__idris_argv; -int idris_numArgs();+int idris_numArgs(void); const char *idris_getArg(int i);  // disable stdin/stdout buffering-void idris_disableBuffering();+void idris_disableBuffering(void);  // Handle stack overflow. // Just reports an error and exits. -void stackOverflow();+void stackOverflow(void);  // I think these names are nicer for an API... 

@@ -11,6 +11,8 @@  #if defined(WIN32) || defined(__WIN32) || defined(__WIN32__) int win_fpoll(void* h);+FILE *win32_u8fopen(const char *path, const char *mode);+FILE *win32_u8popen(const char *path, const char *mode); #else #include <sys/select.h> #endif@@ -21,9 +23,13 @@     printf("%s", str); } -void* fileOpen(char* name, char* mode) {-    FILE* f = fopen(name, mode);-    return (void*)f;+void *fileOpen(char *name, char *mode) {+#if defined(WIN32) || defined(__WIN32) || defined(__WIN32__)+    FILE *f = win32_u8fopen(name, mode);+#else+    FILE *f = fopen(name, mode);+#endif+    return (void *)f; }  void fileClose(void* h) {@@ -82,10 +88,14 @@ #endif } -void* do_popen(const char* cmd, const char* mode) {-    FILE* f = popen(cmd, mode);-//    int d = fileno(f);-//    fcntl(d, F_SETFL, O_NONBLOCK);+void *do_popen(const char *cmd, const char *mode) {+#if defined(WIN32) || defined(__WIN32) || defined(__WIN32__)+    FILE *f = win32_u8popen(cmd, mode);+#else+    FILE *f = popen(cmd, mode);+    //    int d = fileno(f);+    //    fcntl(d, F_SETFL, O_NONBLOCK);+#endif     return f; } 

@@ -193,3 +193,8 @@ int idrnet_errno() {     return errno; }++int idrnet_geteagain() {+    return EAGAIN;+}+

@@ -1,13 +1,13 @@-#include <windows.h> #include <io.h> #include <stdio.h>+#include <windows.h>  // THis file exists to avoid clashes between windows.h and idris_rts.h // -int win_fpoll(void* h)+int win_fpoll(void *h) {-    HANDLE wh =(HANDLE) _get_osfhandle(_fileno((FILE*)h));+    HANDLE wh =(HANDLE) _get_osfhandle(_fileno((FILE *)h));     if (wh == INVALID_HANDLE_VALUE) {         return -1;     }@@ -18,4 +18,34 @@     if (ret == WAIT_TIMEOUT)         return 0;     return -1;+}++int widen_utf8(const char *filename_utf8, LPWSTR *filename_w)+{+    int num_chars = MultiByteToWideChar(CP_UTF8, 0, filename_utf8, -1, 0, 0);+    int size = sizeof(WCHAR);+    *filename_w = (LPWSTR)malloc(size * num_chars);+    MultiByteToWideChar(CP_UTF8, 0, filename_utf8, -1, *filename_w, num_chars);+    return num_chars;+}+FILE *win32_u8fopen(const char *path, const char *mode)+{+    LPWSTR wpath, wmode;+    widen_utf8(path, &wpath);+    widen_utf8(mode, &wmode);+    FILE *f = _wfopen(wpath, wmode);+    free(wpath);+    free(wmode);+    return f;+}++FILE *win32_u8popen(const char *path, const char *mode)+{+    LPWSTR wpath, wmode;+    widen_utf8(path, &wpath);+    widen_utf8(mode, &wmode);+    FILE *f = _wpopen(wpath, wmode);+    free(wpath);+    free(wmode);+    return f; }

@@ -617,6 +617,7 @@ doOp v (LIntCh ITChar) args = doOp v (LIntCh ITNative) args  doOp v LSystemInfo [x] = v ++ "idris_systemInfo(vm, " ++ creg x ++ ")"+doOp v LCrash [x] = "idris_crash(GETSTR(" ++ creg x ++ "))" doOp v LNoOp args = v ++ creg (last args)  -- Pointer primitives (declared as %extern in Builtins.idr)@@ -673,7 +674,7 @@ doOp v (LExternal mpt) [p] | mpt == sUN "prim__asPtr"     = v ++ "MKPTR(vm, GETMPTR("++ creg p ++"))" doOp v (LExternal offs) [p, n] | offs == sUN "prim__ptrOffset"-    = v ++ "MKPTR(vm, GETPTR(" ++ creg p ++ ") + GETINT(" ++ creg n ++ "))"+    = v ++ "MKPTR(vm, (void *)((char *)GETPTR(" ++ creg p ++ ") + GETINT(" ++ creg n ++ ")))" doOp _ op args = error $ "doOp not implemented (" ++ show (op, args) ++ ")"  

@@ -8,6 +8,7 @@ -} module IRTS.CodegenCommon where +import Idris.Core.Evaluate import Idris.Core.TT import IRTS.Defunctionalise import IRTS.Simplified@@ -39,6 +40,7 @@   , liftDecls     :: [(Name, LDecl)]   , interfaces    :: Bool   , exportDecls   :: [ExportIFace]+  , ttDecls       :: [(Name, TTDecl)]   }  type CodeGenerator = CodegenInfo -> IO ()

@@ -52,8 +52,10 @@  -- |  Compile to simplified forms and return CodegenInfo compile :: Codegen -> FilePath -> Maybe Term -> Idris CodegenInfo-compile codegen f mtm-   = do checkMVs  -- check for undefined metavariables+compile codegen f mtm = do+        logCodeGen 1 "Compiling Output."+        iReport 2 "Compiling Output."+        checkMVs  -- check for undefined metavariables         checkTotality -- refuse to compile if there are totality problems         exports <- findExports         let rootNames = case mtm of@@ -72,6 +74,7 @@         flags <- getFlags codegen         hdrs <- getHdrs codegen         impdirs <- allImportDirs+        ttDeclarations <- getDeclarations reachableNames         defsIn <- mkDecls reachableNames         -- if no 'main term' given, generate interface files         let iface = case mtm of@@ -89,9 +92,11 @@         let ctxtIn = addAlist tagged emptyContext          logCodeGen 1 "Defunctionalising"+        iReport 3 "Defunctionalising"         let defuns_in = defunctionalise nexttag ctxtIn         logCodeGen 5 $ show defuns_in         logCodeGen 1 "Inlining"+        iReport 3 "Inlining"         let defuns = inline defuns_in         logCodeGen 5 $ show defuns         logCodeGen 1 "Resolving variables for CG"@@ -108,12 +113,14 @@             Just f -> runIO $ writeFile f (dumpDefuns defuns)         triple <- Idris.AbsSyntax.targetTriple         cpu <- Idris.AbsSyntax.targetCPU-        logCodeGen 1 "Building output"+        logCodeGen 1 "Generating Code."+        iReport 2 "Generating Code."         case checked of             OK c -> do return $ CodegenInfo f outty triple cpu                                             hdrs impdirs objs libs flags                                             NONE c (toAlist defuns)                                             tagged iface exports+                                            ttDeclarations             Error e -> ierror e   where checkMVs = do i <- getIState                       case map fst (idris_metavars i) \\ primDefs of@@ -159,6 +166,12 @@          decls <- mapM build ds          return decls +getDeclarations :: [Name] -> Idris ([(Name, TTDecl)])+getDeclarations used+    = do i <- getIState+         let ds = filter (\(n, (d,_,_,_,_,_)) -> n `elem` used || isCon d) $ ((toAlist . definitions . tt_ctxt) i)+         return ds+ showCaseTrees :: [(Name, LDecl)] -> String showCaseTrees = showSep "\n\n" . map showCT . sortBy (comparing defnRank)   where@@ -258,6 +271,11 @@         | u == txt "assert_unreachable"         -> return $ LError $ "ABORT: Reached an unreachable case in " ++ show top +    (P _ (UN u) _, [_, msg])+        | u == txt "idris_crash"+        -> do msg' <- irTerm top vs env msg+              return $ LOp LCrash [msg']+     -- TMP HACK - until we get inlining.     (P _ (UN r) _, [_, _, _, _, _, arg])         | r == txt "replace"@@ -456,14 +474,14 @@             | otherwise = n          used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)-        fst4 (x,_,_,_,_) = x+        fst4 (x,_,_,_,_,_) = x  irTerm top vs env (P _ n _) = return $ LV (Glob n) irTerm top vs env (V i)     | i >= 0 && i < length env = return $ LV (Glob (env!!i))     | otherwise = ifail $ "bad de bruijn index: " ++ show i -irTerm top vs env (Bind n (Lam _) sc) = LLam [n'] <$> irTerm top vs (n':env) sc+irTerm top vs env (Bind n (Lam _ _) sc) = LLam [n'] <$> irTerm top vs (n':env) sc   where     n' = uniqueName n env 

@@ -92,6 +92,8 @@             | LPar -- evaluate argument anywhere, possibly on another                    -- core or another machine. 'id' is a valid implementation             | LExternal Name+            | LCrash+             | LNoOp   deriving (Show, Eq, Generic) 

@@ -9,6 +9,7 @@ module IRTS.Portable (writePortable) where  import Idris.Core.CaseTree+import Idris.Core.Evaluate import Idris.Core.TT import IRTS.Bytecode import IRTS.CodegenCommon@@ -29,7 +30,7 @@  -- Update the version when the format changes formatVersion :: Int-formatVersion = 1+formatVersion = 3  writePortable :: Handle -> CodegenInfo -> IO () writePortable file ci = do@@ -53,7 +54,8 @@                         "lift-decls" .= (liftDecls ci),                         "defun-decls" .= (defunDecls ci),                         "simple-decls" .= (simpleDecls ci),-                        "bytecode" .= (map toBC (simpleDecls ci))]+                        "bytecode" .= (map toBC (simpleDecls ci)),+                        "tt-decls" .= (ttDecls ci)]  instance ToJSON Name where     toJSON n = toJSON $ showCG n@@ -236,13 +238,13 @@     toJSON (SApp tail name exps) = object ["SApp" .= (tail, name, exps)]     toJSON (SLet lv a b) = object ["SLet" .= (lv, a, b)]     toJSON (SUpdate lv exp) = object ["SUpdate" .= (lv, exp)]-    toJSON (SProj lv i) = object ["DProj" .= (lv, i)]+    toJSON (SProj lv i) = object ["SProj" .= (lv, i)]     toJSON (SCon lv i name vars) = object ["SCon" .= (lv, i, name, vars)]     toJSON (SCase ct lv alts) = object ["SCase" .= (ct, lv, alts)]-    toJSON (SChkCase lv alts) = object ["DChkCase" .= (lv, alts)]+    toJSON (SChkCase lv alts) = object ["SChkCase" .= (lv, alts)]     toJSON (SConst c) = object ["SConst" .= c]     toJSON (SForeign fd ret exps) = object ["SForeign" .= (fd, ret, exps)]-    toJSON (SOp prim vars) = object ["DOp" .= (prim, vars)]+    toJSON (SOp prim vars) = object ["SOp" .= (prim, vars)]     toJSON SNothing = object ["SNothing" .= Null]     toJSON (SError s) = object ["SError" .= s] @@ -279,3 +281,84 @@     toJSON (T i) = object ["T" .= i]     toJSON (L i) = object ["L" .= i]     toJSON Tmp = object ["Tmp" .= Null]++instance ToJSON RigCount where+    toJSON r = object ["RigCount" .= show r]++instance ToJSON Totality where+    toJSON t = object ["Totality" .= show t]++instance ToJSON MetaInformation where+    toJSON m = object ["MetaInformation" .= show m]++instance ToJSON Def where+    toJSON (Function ty tm) = object ["Function" .= (ty, tm)]+    toJSON (TyDecl nm ty) = object ["TyDecl" .= (nm, ty)]+    toJSON (Operator ty n f) = Null -- Operator and CaseOp omits same values as in IBC.hs+    toJSON (CaseOp info ty argTy _ _ cdefs) = object ["CaseOp" .= (info, ty, argTy, cdefs)]++instance (ToJSON t) => ToJSON (TT t) where+    toJSON (P nt name term) = object ["P" .= (nt, name, term)]+    toJSON (V n) = object ["V" .= n]+    toJSON (Bind n b tt) = object ["Bind" .= (n, b, tt)]+    toJSON (App s t1 t2) = object ["App" .= (s, t1, t2)]+    toJSON (Constant c) = object ["Constant" .= c]+    toJSON (Proj tt n) = object ["Proj" .= (tt, n)]+    toJSON Erased = object ["Erased" .= Null]+    toJSON Impossible = object ["Impossible" .= Null]+    toJSON (Inferred tt) = object ["Inferred" .= tt]+    toJSON (TType u) = object ["TType" .= u]+    toJSON (UType u) = object ["UType" .= (show u)]++instance ToJSON UExp where+    toJSON (UVar src n) = object ["UVar" .= (src, n)]+    toJSON (UVal n) = object ["UVal" .= n]+++instance (ToJSON t) => ToJSON (AppStatus t) where+    toJSON Complete = object ["Complete" .= Null]+    toJSON MaybeHoles = object ["MaybeHoles" .= Null]+    toJSON (Holes ns) = object ["Holes" .= ns]++instance (ToJSON t) => ToJSON (Binder t) where+    toJSON (Lam rc bty) = object ["Lam" .= (rc, bty)]+    toJSON (Pi c i t k) = object ["Pi" .= (c, i, t, k)]+    toJSON (Let t v) = object ["Let" .= (t, v)]+    toJSON (NLet t v) = object ["NLet" .= (t, v)]+    toJSON (Hole t) = object ["Hole" .= (t)]+    toJSON (GHole l ns t) = object ["GHole" .= (l, ns, t)]+    toJSON (Guess t v) = object ["Guess" .= (t, v)]+    toJSON (PVar rc t) = object ["PVar" .= (rc, t)]+    toJSON (PVTy t) = object ["PVTy" .= (t)]++instance ToJSON ImplicitInfo where+    toJSON (Impl a b c) = object ["Impl" .= (a, b, c)]++instance ToJSON NameType where+    toJSON Bound = object ["Bound" .= Null]+    toJSON Ref = object ["Ref" .= Null]+    toJSON (DCon a b c) = object ["DCon" .= (a, b, c)]+    toJSON (TCon a b) = object ["TCon" .= (a, b)]++instance ToJSON CaseDefs where+    toJSON (CaseDefs rt ct) = object ["Runtime" .= rt, "Compiletime" .= ct]++instance (ToJSON t) => ToJSON (SC' t) where+    toJSON (Case ct n alts) = object ["Case" .= (ct, n, alts)]+    toJSON (ProjCase t alts) = object ["ProjCase" .= (t, alts)]+    toJSON (STerm t) = object ["STerm" .= t]+    toJSON (UnmatchedCase s) = object ["UnmatchedCase" .= s]+    toJSON ImpossibleCase = object ["ImpossibleCase" .= Null]++instance (ToJSON t) => ToJSON (CaseAlt' t) where+    toJSON (ConCase n c ns sc) = object ["ConCase" .= (n, c, ns, sc)]+    toJSON (FnCase n ns sc) = object ["FnCase" .= (n, ns, sc)]+    toJSON (ConstCase c sc) = object ["ConstCase" .= (c, sc)]+    toJSON (SucCase n sc) = object ["SucCase" .= (n, sc)]+    toJSON (DefaultCase sc) = object ["DefaultCase" .=  sc]++instance ToJSON CaseInfo where+    toJSON (CaseInfo a b c) = object ["CaseInfo" .= (a, b, c)]++instance ToJSON Accessibility where+    toJSON a = object ["Accessibility" .= show a]

@@ -42,15 +42,15 @@ data SDecl = SFun Name [Name] Int SExp   deriving Show -hvar :: State (DDefs, Int) Int-hvar = do (l, h) <- get-          put (l, h + 1)-          return h  ldefs :: State (DDefs, Int) DDefs ldefs = do (l, h) <- get            return l +-- | Simplify an expression by let-binding argument expressions that+-- are not variables+-- The boolean parameter indicates whether the expression is at tail+-- call position. simplify :: Bool -> DExp -> State (DDefs, Int) SExp simplify tl (DV (Loc i)) = return (SV (Loc i)) simplify tl (DV (Glob x))@@ -58,67 +58,62 @@          case lookupCtxtExact x ctxt of               Just (DConstructor _ t 0) -> return $ SCon Nothing t x []               _ -> return $ SV (Glob x)-simplify tl (DApp tc n args) = do args' <- mapM sVar args-                                  mkapp (SApp (tl || tc) n) args'+simplify tl (DApp tc n args) = bindExprs args (SApp (tl || tc) n) simplify tl (DForeign ty fn args)-                            = do args' <- mapM sVar (map snd args)-                                 let fargs = zip (map fst args) args'-                                 mkfapp (SForeign ty fn) fargs+    = let (fdescs, exprs) = unzip args+      in bindExprs exprs (\vars -> SForeign ty fn (zip fdescs vars)) simplify tl (DLet n v e) = do v' <- simplify False v                               e' <- simplify tl e                               return (SLet (Glob n) v' e') simplify tl (DUpdate n e) = do e' <- simplify False e                                return (SUpdate (Glob n) e')-simplify tl (DC loc i n args) = do args' <- mapM sVar args-                                   mkapp (SCon loc i n) args'-simplify tl (DProj t i) = do v <- sVar t-                             case v of-                                (x, Nothing) -> return (SProj x i)-                                (Glob x, Just e) ->-                                    return (SLet (Glob x) e (SProj (Glob x) i))-simplify tl (DCase up e alts) = do v <- sVar e-                                   alts' <- mapM (sAlt tl) alts-                                   case v of-                                      (x, Nothing) -> return (SCase up x alts')-                                      (Glob x, Just e) ->-                                          return (SLet (Glob x) e (SCase up (Glob x) alts'))+simplify tl (DC loc i n args) = bindExprs args (SCon loc i n)+simplify tl (DProj t i) = bindExpr t (\var -> SProj var i)+simplify tl (DCase up e alts)+    = do alts' <- mapM (sAlt tl) alts+         bindExpr e (\var -> SCase up var alts') simplify tl (DChkCase e alts)-                           = do v <- sVar e-                                alts' <- mapM (sAlt tl) alts-                                case v of-                                    (x, Nothing) -> return (SChkCase x alts')-                                    (Glob x, Just e) ->-                                        return (SLet (Glob x) e (SChkCase (Glob x) alts'))+    = do alts' <- mapM (sAlt tl) alts+         bindExpr e (\var -> SChkCase var alts') simplify tl (DConst c) = return (SConst c)-simplify tl (DOp p args) = do args' <- mapM sVar args-                              mkapp (SOp p) args'+simplify tl (DOp p args) = bindExprs args (SOp p) simplify tl DNothing = return SNothing simplify tl (DError str) = return $ SError str -sVar (DV (Glob x))++-- | Let-bind a list of expressions to variables and construct the+-- inner expression with the bound variables.+-- If an expression in the list is already a variable we don’t bind it+-- again.+bindExprs :: [DExp] -> ([LVar] -> SExp) -> State (DDefs, Int) SExp+bindExprs es f = bindExprs' es f [] where+    bindExprs' [] f vars = return $ f (reverse vars)+    bindExprs' (e:es) f vars =+        bindExprM e (\var -> bindExprs' es f (var:vars))++-- | Special case of 'bindExprs' for just one expression+bindExpr :: DExp -> (LVar -> SExp) -> State (DDefs, Int) SExp+bindExpr e f = bindExprM e (return . f)++bindExprM :: DExp -> (LVar -> State (DDefs, Int) SExp) -> State (DDefs, Int) SExp+bindExprM (DV (Glob x)) f     = do ctxt <- ldefs          case lookupCtxtExact x ctxt of-              Just (DConstructor _ t 0) -> sVar (DC Nothing t x [])-              _ -> return (Glob x, Nothing)-sVar (DV x) = return (x, Nothing)-sVar e = do e' <- simplify False e-            i <- hvar-            return (Glob (sMN i "R"), Just e')+              Just (DConstructor _ t 0) -> bindExprM (DC Nothing t x []) f+              _ -> f (Glob x)+bindExprM (DV var) f = f var+bindExprM e f =+    do e' <- simplify False e+       var <- freshVar+       f' <- f var+       return $ SLet var e' f'+    where+        freshVar = do (defs, i) <- get+                      put (defs, i + 1)+                      return (Glob (sMN i "R")) -mkapp f args = mkapp' f args [] where-   mkapp' f [] args = return $ f (reverse args)-   mkapp' f ((x, Nothing) : xs) args = mkapp' f xs (x : args)-   mkapp' f ((x, Just e) : xs) args-       = do sc <- mkapp' f xs (x : args)-            return (SLet x e sc) -mkfapp f args = mkapp' f args [] where-   mkapp' f [] args = return $ f (reverse args)-   mkapp' f ((ty, (x, Nothing)) : xs) args = mkapp' f xs ((ty, x) : args)-   mkapp' f ((ty, (x, Just e)) : xs) args-       = do sc <- mkapp' f xs ((ty, x) : args)-            return (SLet x e sc)-+sAlt :: Bool -> DAlt -> State (DDefs, Int) SAlt sAlt tl (DConCase i n args e) = do e' <- simplify tl e                                    return (SConCase (-1) i n args e') sAlt tl (DConstCase c e) = do e' <- simplify tl e

@@ -6,7 +6,7 @@ Maintainer  : The Idris Community. -} {-# LANGUAGE CPP #-}-module IRTS.System( getDataFileName+module IRTS.System( getIdrisDataFileByName                   , getCC                   , getLibFlags                   , getIdrisDataDir@@ -41,6 +41,11 @@       ddir <- getDataDir       return ddir     Just ddir -> return ddir++getIdrisDataFileByName :: String -> IO FilePath+getIdrisDataFileByName fn = do+  dir <- getIdrisDataDir+  return $ dir </> fn  overrideIdrisSubDirWith :: String  -- ^ Sub directory in `getDataDir` location.                         -> String  -- ^ Environment variable to get new location from.

@@ -1,3 +1,4 @@+{-# LANGUAGE MultiParamTypeClasses #-} {-| Module      : Idris.ASTUtils Description : This implements just a few basic lens-like concepts to ease state updates. Similar to fclabels in approach, just without the extra dependency.@@ -148,7 +149,7 @@ -- -- This has a terrible name, but I'm not sure of a better one that -- isn't confusingly close to tt_ctxt-known_terms :: Field IState (Ctxt (Def, Injectivity, Accessibility, Totality, MetaInformation))+known_terms :: Field IState (Ctxt (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation)) known_terms = Field (definitions . tt_ctxt)                     (\v state -> state {tt_ctxt = (tt_ctxt state) {definitions = v}}) 

@@ -5,9 +5,9 @@ License     : BSD3 Maintainer  : The Idris Community. -}-{-# LANGUAGE DeriveFunctor, FlexibleInstances, MultiParamTypeClasses,-             PatternGuards, TypeSynonymInstances #-} +{-# LANGUAGE DeriveFunctor, PatternGuards #-}+ module Idris.AbsSyntax(     module Idris.AbsSyntax   , module Idris.AbsSyntaxTree@@ -15,37 +15,33 @@  import Idris.AbsSyntaxTree import Idris.Colours-import Idris.Core.Elaborate hiding (Tactic(..)) import Idris.Core.Evaluate import Idris.Core.TT-import Idris.Core.Typecheck import Idris.Docstrings import Idris.IdeMode hiding (Opt(..)) import IRTS.CodegenCommon -import Util.DynamicLinker-import Util.Pretty-import Util.ScreenSize-import Util.System+import System.Directory (canonicalizePath, doesFileExist)+import System.IO  import Control.Applicative-import Control.Monad (liftM3) import Control.Monad.State-import Data.Char+import Prelude hiding (Applicative, Foldable, Traversable, (<$>))+ import Data.Either-import Data.Generics.Uniplate.Data (descend, descendM) import Data.List hiding (insert, union) import qualified Data.Map as M import Data.Maybe import qualified Data.Set as S import qualified Data.Text as T-import Data.Word (Word)+import System.IO.Error (tryIOError)++import Data.Generics.Uniplate.Data (descend, descendM)+ import Debug.Trace-import Network (PortID(PortNumber))-import System.Console.Haskeline-import System.Directory (canonicalizePath, doesFileExist)-import System.IO-import System.IO.Error (ioeGetErrorString, isUserError, tryIOError)+import Util.DynamicLinker+import Util.Pretty+import Util.System  getContext :: Idris Context getContext = do i <- getIState; return (tt_ctxt i)@@ -91,9 +87,9 @@                          Just x -> do putIState $ i { idris_dynamic_libs = x:ls }                                       return (Left x)     where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib-          findDyLib []         l                     = Nothing-          findDyLib (lib:libs) l | l == lib_name lib = Just lib-                                 | otherwise         = findDyLib libs l+          findDyLib []         _                     = Nothing+          findDyLib (lib:libs') l | l == lib_name lib = Just lib+                                  | otherwise         = findDyLib libs' l  getAutoImports :: Idris [FilePath] getAutoImports = do i <- getIState@@ -102,7 +98,6 @@ addAutoImport :: FilePath -> Idris () addAutoImport fp = do i <- getIState                       let opts = idris_options i-                      let autoimps = opt_autoImport opts                       put (i { idris_options = opts { opt_autoImport =                                                        fp : opt_autoImport opts } } ) @@ -142,14 +137,10 @@           putIState $ i { idris_imported = nub $ (f, pub) : idris_imported i }  addLangExt :: LanguageExt -> Idris ()-addLangExt TypeProviders = do i <- getIState-                              putIState $ i {-                                idris_language_extensions = TypeProviders : idris_language_extensions i-                              }-addLangExt ErrorReflection = do i <- getIState-                                putIState $ i {-                                  idris_language_extensions = ErrorReflection : idris_language_extensions i-                                }+addLangExt e = do i <- getIState+                  putIState $ i {+                    idris_language_extensions = e : idris_language_extensions i+                  }  -- | Transforms are organised by the function being applied on the lhs -- of the transform, to make looking up appropriate transforms quicker@@ -162,10 +153,18 @@                 putIState $ i { idris_transforms = addDef basefn t'                                                           (idris_transforms i) } +-- | Add transformation rules from a definition, which will reverse the+-- definition for an error to make it more readable addErrRev :: (Term, Term) -> Idris () addErrRev t = do i <- getIState                  putIState $ i { idris_errRev = t : idris_errRev i } +-- | Say that the name should always be reduced in error messages, to+-- help readability/error reflection+addErrReduce :: Name -> Idris ()+addErrReduce t = do i <- getIState+                    putIState $ i { idris_errReduce = t : idris_errReduce i }+ addErasureUsage :: Name -> Int -> Idris () addErasureUsage n i = do ist <- getIState                          putIState $ ist { idris_erasureUsed = (n, i) : idris_erasureUsed ist }@@ -254,7 +253,7 @@     let cs = idris_coercions i         (fn,_) = unApply (getRetTy ty) in         findCoercions fn cs-    where findCoercions t [] = []+    where findCoercions _ [] = []           findCoercions t (n : ns) =              let ps = case lookupTy n (tt_ctxt i) of                         [ty'] -> case unApply (getRetTy (normalise (tt_ctxt i) [] ty')) of@@ -326,10 +325,10 @@               do let (fx, _) = unApply x                  let (fy, _) = unApply y                  case (fx, fy) of-                      (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n)+                      (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n')                       (P (TCon _ _) n _, Constant _) -> errWhen True                       (Constant _, P (TCon _ _) n' _) -> errWhen True-                      (P (DCon _ _ _) n _, P (DCon _ _ _) n' _) -> errWhen (n/=n)+                      (P (DCon _ _ _) n _, P (DCon _ _ _) n' _) -> errWhen (n/=n')                       _ -> return ()                where errWhen True@@ -357,12 +356,6 @@                         -- will always be one of those two, thus no extra case     putIState $ i { idris_function_errorhandlers = newHandlers } -getFunctionErrorHandlers :: Name -> Name -> Idris [Name]-getFunctionErrorHandlers f arg = do i <- getIState-                                    return . maybe [] S.toList $-                                     undefined --lookup arg =<< lookupCtxtExact f (idris_function_errorhandlers i)-- -- | Trace all the names in a call graph starting at the given name getAllNames :: Name -> Idris [Name] getAllNames n = do i <- getIState@@ -389,7 +382,7 @@                    case getCGAllNames i n of                         Just ns -> return ns                         Nothing -> case lookupCtxtExact n (idris_callgraph i) of-                                        Just ci -> +                                        Just ci ->                                           do more <- mapM (allNames (n:ns)) (calls ci)                                              let ns' = nub (n : concat more)                                              addCGAllNames i n ns'@@ -418,7 +411,7 @@         putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }  getNameHints :: IState -> Name -> [Name]-getNameHints i (UN arr) | arr == txt "->" = [sUN "f",sUN "g"]+getNameHints _ (UN arr) | arr == txt "->" = [sUN "f",sUN "g"] getNameHints i n =         case lookupCtxt n (idris_namehints i) of              [ns] -> ns@@ -434,7 +427,6 @@   i <- getIState   return $ lookupCtxtExact n (idris_deprecated i) - addFragile :: Name -> String -> Idris () addFragile n reason = do   i <- getIState@@ -446,15 +438,15 @@   return $ lookupCtxtExact n (idris_fragile i)  push_estack :: Name -> Bool -> Idris ()-push_estack n impl+push_estack n implementation     = do i <- getIState-         putIState (i { elab_stack = (n, impl) : elab_stack i })+         putIState (i { elab_stack = (n, implementation) : elab_stack i })  pop_estack :: Idris () pop_estack = do i <- getIState                 putIState (i { elab_stack = ptail (elab_stack i) })     where ptail [] = []-          ptail (x : xs) = xs+          ptail (_ : xs) = xs  -- | Add an interface implementation function. --@@ -519,10 +511,25 @@ addInterface n i    = do ist <- getIState         let i' = case lookupCtxt n (idris_interfaces ist) of-                      [c] -> c { interface_implementations = interface_implementations i }+                      [c] -> i { interface_implementations = interface_implementations c +++                                                             interface_implementations i }                       _ -> i         putIState $ ist { idris_interfaces = addDef n i' (idris_interfaces ist) } +updateIMethods :: Name -> [(Name, PTerm)] -> Idris ()+updateIMethods n meths+   = do ist <- getIState+        let i = case lookupCtxtExact n (idris_interfaces ist) of+                     Just c -> c { interface_methods = update (interface_methods c) }+                     Nothing -> error "Can't happen updateIMethods"+        putIState $ ist { idris_interfaces = addDef n i (idris_interfaces ist) }+  where+    update [] = []+    update (m@(n, (b, opts, t)) : rest)+        | Just ty <- lookup n meths+             = (n, (b, opts, ty)) : update rest+        | otherwise = m : update rest+ addRecord :: Name -> RecordInfo -> Idris () addRecord n ri = do ist <- getIState                     putIState $ ist { idris_records = addDef n ri (idris_records ist) }@@ -550,7 +557,7 @@                 when (notDef (ibc_write i)) $                   putIState $ i { ibc_write = ibc : ibc_write i }    where notDef [] = True-         notDef (IBCDef n': is) | n == n' = False+         notDef (IBCDef n': _) | n == n' = False          notDef (_ : is) = notDef is addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i } @@ -687,7 +694,7 @@ clearPTypes = do i <- get                  let ctxt = tt_ctxt i                  put (i { tt_ctxt = mapDefCtxt pErase ctxt })-   where pErase (CaseOp c t tys orig tot cds)+   where pErase (CaseOp c t tys orig _ cds)             = CaseOp c t tys orig [] (pErase' cds)          pErase x = x          pErase' (CaseDefs (cs, c) rs)@@ -703,7 +710,7 @@              _ -> return ()  isUndefined :: FC -> Name -> Idris Bool-isUndefined fc n+isUndefined _ n     = do i <- getContext          case lookupTyExact n i of              Just _ -> return False@@ -760,7 +767,7 @@         tidyNames used (Bind n b sc)             = let n' = uniqueNameSet n used in                   Bind n' b $ tidyNames (S.insert n' used) sc-        tidyNames used b = b+        tidyNames _    b = b  solveDeferred :: FC -> Name -> Idris () solveDeferred fc n@@ -1028,18 +1035,32 @@ targetCPU = do i <- getIState                return (opt_cpu (idris_options i)) -verbose :: Idris Bool-verbose = do i <- getIState-             -- Quietness overrides verbosity-             return (not (opt_quiet (idris_options i)) &&-                     opt_verbose (idris_options i))+verbose :: Idris Int+verbose = do+  i <- getIState+  -- Quietness overrides verbosity+  let quiet = opt_quiet   $ idris_options i+  if quiet+    then return $ 0+    else return $ (opt_verbose $ idris_options i) -setVerbose :: Bool -> Idris ()-setVerbose t = do i <- getIState-                  let opts = idris_options i-                  let opt' = opts { opt_verbose = t }-                  putIState $ i { idris_options = opt' }+setVerbose :: Int -> Idris ()+setVerbose t = do+  i <- getIState+  let opts = idris_options i+  let opt' = opts { opt_verbose = t }+  putIState $ i { idris_options = opt' } +iReport :: Int -> String -> Idris ()+iReport level msg = do+  verbosity <- verbose+  i <- getIState+  when (level <= verbosity) $+    case idris_outputmode i of+      RawOutput h -> runIO $ hPutStrLn h msg+      IdeMode n h -> runIO . hPutStrLn h $ convSExp "write-string" msg n+  return ()+ typeInType :: Idris Bool typeInType = do i <- getIState                 return (opt_typeintype (idris_options i))@@ -1134,7 +1155,6 @@           setColour' PromptColour    c t = t { promptColour = c }           setColour' PostulateColour c t = t { postulateColour = c } - logLvl :: Int -> String -> Idris () logLvl = logLvlCats [] @@ -1168,7 +1188,7 @@            -> Int      -- ^ The Logging level the message should appear.            -> String   -- ^ The message to show the developer.            -> Idris ()-logLvlCats cs l str = do+logLvlCats cs l msg = do     i <- getIState     let lvl  = opt_logLevel (idris_options i)     let cats = opt_logcats (idris_options i)@@ -1176,9 +1196,9 @@       when (inCat cs cats || null cats) $         case idris_outputmode i of           RawOutput h -> do-            runIO $ hPutStrLn h str+            runIO $ hPutStrLn h msg           IdeMode n h -> do-            let good = SexpList [IntegerAtom (toInteger l), toSExp str]+            let good = SexpList [IntegerAtom (toInteger l), toSExp msg]             runIO . hPutStrLn h $ convSExp "log" good n   where     inCat :: [LogCat] -> [LogCat] -> Bool@@ -1200,7 +1220,30 @@                    let opt' = opts { opt_typecase = t }                    putIState $ i { idris_options = opt' } +getIndentWith :: Idris Int+getIndentWith = do+  i <- getIState+  return $ interactiveOpts_indentWith (idris_interactiveOpts i) +setIndentWith :: Int -> Idris ()+setIndentWith indentWith = do+  i <- getIState+  let opts = idris_interactiveOpts i+  let opts' = opts { interactiveOpts_indentWith = indentWith }+  putIState $ i { idris_interactiveOpts = opts' }++getIndentClause :: Idris Int+getIndentClause = do+  i <- getIState+  return $ interactiveOpts_indentClause (idris_interactiveOpts i)++setIndentClause :: Int -> Idris ()+setIndentClause indentClause = do+  i <- getIState+  let opts = idris_interactiveOpts i+  let opts' = opts { interactiveOpts_indentClause = indentClause }+  putIState $ i { idris_interactiveOpts = opts' }+ -- Dealing with parameters  expandParams :: (Name -> Name) -> [(Name, PTerm)] ->@@ -1296,8 +1339,8 @@      nseq x y = nsroot x == nsroot y -    enTacImp ql (TacImp aos st scr)  = TacImp aos st (en ql scr)-    enTacImp ql other                = other+    enTacImp ql (TacImp aos st scr rig) = TacImp aos st (en ql scr) rig+    enTacImp ql other                   = other  expandParamsD :: Bool -> -- True = RHS only                  IState ->@@ -1465,10 +1508,10 @@        putIState $ i { idris_statics = addDef n stpos (idris_statics i) }        addIBC (IBCStatic n)   where-    initStatics (Bind n (Pi _ ty _) sc) (PPi p n' fc t s)+    initStatics (Bind n (Pi _ _ ty _) sc) (PPi p n' fc t s)             | n /= n' = let (static, dynamic) = initStatics sc (PPi p n' fc t s) in                             (static, (n, ty) : dynamic)-    initStatics (Bind n (Pi _ ty _) sc) (PPi p n' fc _ s)+    initStatics (Bind n (Pi _ _ ty _) sc) (PPi p n' fc _ s)             = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in                   if pstatic p == Static then ((n, ty) : static, dynamic)                     else if (not (searchArg p))@@ -1484,16 +1527,16 @@             getNamePos i ps (P _ n _ : as)                  | i `elem` ps = n : getNamePos (i + 1) ps as             getNamePos i ps (_ : as) = getNamePos (i + 1) ps as-    getParamNames ist (Bind t (Pi _ (P _ n _) _) sc)+    getParamNames ist (Bind t (Pi _ _ (P _ n _) _) sc)        = n : getParamNames ist sc     getParamNames ist _ = [] -    getNamesFrom i ps (Bind n (Pi _ _ _) sc)+    getNamesFrom i ps (Bind n (Pi _ _ _ _) sc)        | i `elem` ps = n : getNamesFrom (i + 1) ps sc        | otherwise = getNamesFrom (i + 1) ps sc     getNamesFrom i ps sc = [] -    freeArgNames (Bind n (Pi _ ty _) sc)+    freeArgNames (Bind n (Pi _ _ ty _) sc)           = nub $ freeNames ty ++ freeNames sc -- treat '->' as fn here     freeArgNames tm = let (_, args) = unApply tm in                           concatMap freeNames args@@ -1501,11 +1544,11 @@     -- if a name appears in an interface or tactic implicit index, it doesn't     -- affect its 'uniquely inferrable' from a static status since these are     -- resolved by searching.-    searchArg (Constraint _ _) = True-    searchArg (TacImp _ _ _) = True+    searchArg (Constraint _ _ _) = True+    searchArg (TacImp _ _ _ _) = True     searchArg _ = False -    staticList sts (Bind n (Pi _ _ _) sc) = (n `elem` sts) : staticList sts sc+    staticList sts (Bind n (Pi _ _ _ _) sc) = (n `elem` sts) : staticList sts sc     staticList _ _ = []  -- Dealing with implicit arguments@@ -1537,14 +1580,14 @@          -- if all of args in ns, then add it          doAdd (UConstraint c args : cs) ns t              | all (\n -> elem n ns) args-                   = PPi (Constraint [] Dynamic) (sMN 0 "cu") NoFC+                   = PPi (Constraint [] Dynamic RigW) (sMN 0 "cu") NoFC                          (mkConst c args) (doAdd cs ns t)              | otherwise = doAdd cs ns t           mkConst c args = PApp fc (PRef fc [] c)                            (map (PExp 0 [] (sMN 0 "carg") . PRef fc []) args) -         getConstraints (PPi (Constraint _ _) _ _ c sc)+         getConstraints (PPi (Constraint _ _ _) _ _ c sc)              = getcapp c ++ getConstraints sc          getConstraints (PPi _ _ _ c sc) = getConstraints sc          getConstraints _ = []@@ -1613,25 +1656,25 @@         scopedimpl (Just i) = not (toplevel_imp i)         scopedimpl _ = False -        getImps (Bind n (Pi i _ _) sc) imps+        getImps (Bind n (Pi _ i _ _) sc) imps              | scopedimpl i = getImps sc imps-        getImps (Bind n (Pi _ t _) sc) imps+        getImps (Bind n (Pi _ _ t _) sc) imps             | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps          where-            argInfo n (Imp opt _ _ _ _) Placeholder+            argInfo n (Imp opt _ _ _ _ _) Placeholder                    = (True, PImp 0 True opt n Placeholder)-            argInfo n (Imp opt _ _ _ _) t'+            argInfo n (Imp opt _ _ _ _ _) t'                    = (False, PImp (getPriority i t') True opt n t')-            argInfo n (Exp opt _ _) t'+            argInfo n (Exp opt _ _ _) t'                    = (InaccessibleArg `elem` opt,                           PExp (getPriority i t') opt n t')-            argInfo n (Constraint opt _) t'+            argInfo n (Constraint opt _ _) t'                    = (InaccessibleArg `elem` opt,                           PConstraint 10 opt n t')-            argInfo n (TacImp opt _ scr) t'+            argInfo n (TacImp opt _ scr _) t'                    = (InaccessibleArg `elem` opt,                           PTacImplicit 10 opt n scr t')-        getImps (Bind n (Pi _ t _) sc) imps = impBind n t : getImps sc imps+        getImps (Bind n (Pi _ _ t _) sc) imps = impBind n t : getImps sc imps            where impBind n t = (True, PImp 1 True [] n Placeholder)         getImps sc tm = [] @@ -1714,13 +1757,13 @@        = do (decls, ns) <- get             let isn = nub (implNamesIn uvars ty)             put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))-    imps top env (PPi (Imp l _ _ _ _) n _ ty sc)+    imps top env (PPi (Imp l _ _ _ _ _) n _ ty sc)         = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]              (decls , ns) <- get              put (PImp (getPriority ist ty) True l n Placeholder : decls,                   nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))              imps True (n:env) sc-    imps top env (PPi (Exp l _ _) n _ ty sc)+    imps top env (PPi (Exp l _ _ _) n _ ty sc)         = do let isn = nub (implNamesIn uvars ty ++ case sc of                             (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]                             _ -> [])@@ -1728,7 +1771,7 @@              put (PExp (getPriority ist ty) l n Placeholder : decls,                   nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))              imps True (n:env) sc-    imps top env (PPi (Constraint l _) n _ ty sc)+    imps top env (PPi (Constraint l _ _) n _ ty sc)         = do let isn = nub (implNamesIn uvars ty ++ case sc of                             (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]                             _ -> [])@@ -1736,7 +1779,7 @@              put (PConstraint 10 l n Placeholder : decls,                   nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))              imps True (n:env) sc-    imps top env (PPi (TacImp l _ scr) n _ ty sc)+    imps top env (PPi (TacImp l _ scr _) n _ ty sc)         = do let isn = nub (implNamesIn uvars ty ++ case sc of                             (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]                             _ -> [])@@ -1908,7 +1951,8 @@     ai inpat qq env ds (PPi p n nfc ty sc)       = let ty' = ai inpat qq env ds ty             env' = if n `elem` imp_meths then env-                      else ((n, Just ty) : env)+                      else+                      ((n, Just ty) : env)             sc' = ai inpat qq env' ds sc in             PPi p n nfc ty' sc'     ai inpat qq env ds (PGoal fc r n sc)@@ -2136,7 +2180,7 @@ stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where     su :: PTerm -> PTerm     su tm@(PRef fc hl f)-       | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)+       | (Bind n (Pi _ _ t _) sc :_) <- lookupTy f (tt_ctxt i)           = Placeholder        | (TType _ : _) <- lookupTy f (tt_ctxt i),          not (implicitable f)@@ -2149,8 +2193,12 @@        -- check will not necessarily fully resolve constructor names,        -- and these bare names will otherwise get in the way of        -- impossbility checking.-       | canBeDConName fn ctxt+       | -- Just fn <- getFn f,+         canBeDConName fn ctxt           = PApp fc f (fmap (fmap su) args)+      where getFn (PRef _ _ fn) = Just fn+            getFn (PApp _ f args) = getFn f+            getFn _ = Nothing     su (PApp fc f args)           = PHidden (PApp fc f args)     su (PAlternative ms b alts)@@ -2216,9 +2264,10 @@ instance Monad (EitherErr a) where     return = RightOK -    (LeftErr e) >>= k = LeftErr e+    (LeftErr e) >>= _ = LeftErr e     RightOK v   >>= k = k v +toEither :: EitherErr a b -> Either a b toEither (LeftErr e)  = Left e toEither (RightOK ho) = Right ho @@ -2359,6 +2408,8 @@                    PPi p x' fc (sm (x':xs) (substMatch x (PRef emptyFC [] x') t))                                (sm (x':xs) (substMatch x (PRef emptyFC [] x') sc))          | otherwise = PPi p x fc (sm xs t) (sm (x : xs) sc)+    sm xs (PLet fc x xfc val t sc)+         = PLet fc x xfc (sm xs val) (sm xs t) (sm xs sc)     sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)     sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)     sm xs (PIfThenElse fc c t f) = PIfThenElse fc (sm xs c) (sm xs t) (sm xs f)@@ -2429,7 +2480,7 @@   -- looking for too long...)   initN (UN n) l = UN $ txt (str n ++ show l)   initN (MN i s) l = MN (i+l) s-  initN n l = n+  initN n _ = n    -- FIXME: Probably ought to do this for completeness! It's fine as   -- long as there are no bindings inside tactics though.@@ -2537,50 +2588,49 @@    mkUniq ql nmap tm = descendM (mkUniq ql nmap) tm - getFile :: Opt -> Maybe String-getFile (Filename str) = Just str+getFile (Filename s) = Just s getFile _ = Nothing  getBC :: Opt -> Maybe String-getBC (BCAsm str) = Just str+getBC (BCAsm s) = Just s getBC _ = Nothing  getOutput :: Opt -> Maybe String-getOutput (Output str) = Just str+getOutput (Output s) = Just s getOutput _ = Nothing  getIBCSubDir :: Opt -> Maybe String-getIBCSubDir (IBCSubDir str) = Just str+getIBCSubDir (IBCSubDir s) = Just s getIBCSubDir _ = Nothing  getImportDir :: Opt -> Maybe String-getImportDir (ImportDir str) = Just str+getImportDir (ImportDir s) = Just s getImportDir _ = Nothing  getSourceDir :: Opt -> Maybe String-getSourceDir (SourceDir str) = Just str+getSourceDir (SourceDir s) = Just s getSourceDir _ = Nothing  getPkgDir :: Opt -> Maybe String-getPkgDir (Pkg str) = Just str+getPkgDir (Pkg s) = Just s getPkgDir _ = Nothing  getPkg :: Opt -> Maybe (Bool, String)-getPkg (PkgBuild   str) = Just (False, str)-getPkg (PkgInstall str) = Just (True, str)+getPkg (PkgBuild s)   = Just (False, s)+getPkg (PkgInstall s) = Just (True, s) getPkg _ = Nothing  getPkgClean :: Opt -> Maybe String-getPkgClean (PkgClean str) = Just str+getPkgClean (PkgClean s) = Just s getPkgClean _ = Nothing  getPkgREPL :: Opt -> Maybe String-getPkgREPL (PkgREPL str) = Just str+getPkgREPL (PkgREPL s) = Just s getPkgREPL _ = Nothing  getPkgCheck :: Opt -> Maybe String-getPkgCheck (PkgCheck str) = Just str+getPkgCheck (PkgCheck s) = Just s getPkgCheck _              = Nothing  -- | Returns None if given an Opt which is not PkgMkDoc@@ -2608,7 +2658,6 @@ getConsoleWidth (UseConsoleWidth x) = Just x getConsoleWidth _ = Nothing - getExecScript :: Opt -> Maybe String getExecScript (InterpretScript expr) = Just expr getExecScript _ = Nothing@@ -2657,7 +2706,7 @@ -- Get the first valid port getPort :: [Opt] -> Maybe REPLPort getPort []            = Nothing-getPort (Port p : xs) = Just p+getPort (Port p : _ ) = Just p getPort (_      : xs) = getPort xs  opt :: (Opt -> Maybe a) -> [Opt] -> [a]

@@ -5,50 +5,47 @@ License     : BSD3 Maintainer  : The Idris Community. -}-{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveGeneric,-             FlexibleInstances, MultiParamTypeClasses, PatternGuards,-             TypeSynonymInstances #-} +{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveGeneric, PatternGuards #-}+ module Idris.AbsSyntaxTree where -import Idris.Colours import Idris.Core.Elaborate hiding (Tactic(..)) import Idris.Core.Evaluate import Idris.Core.TT-import Idris.Core.Typecheck import Idris.Docstrings import IRTS.CodegenCommon import IRTS.Lang import Util.DynamicLinker import Util.Pretty -import Prelude hiding ((<$>))+import Idris.Colours +import System.IO++import Prelude hiding (Foldable, Traversable, (<$>))+ import Control.Applicative ((<|>)) import qualified Control.Monad.Trans.Class as Trans (lift) import Control.Monad.Trans.Except import Control.Monad.Trans.State.Strict import Data.Char import Data.Data (Data)-import Data.Either+ import Data.Foldable (Foldable) import Data.Function (on) import Data.Generics.Uniplate.Data (children, universe) import Data.List hiding (group) import qualified Data.Map.Strict as M-import Data.Maybe (fromMaybe, mapMaybe, maybeToList)+import Data.Maybe (mapMaybe, maybeToList) import qualified Data.Set as S import qualified Data.Text as T import Data.Traversable (Traversable) import Data.Typeable-import Data.Word (Word)-import Debug.Trace import GHC.Generics (Generic) import Network.Socket (PortNumber)-import System.Console.Haskeline-import System.IO-import Text.PrettyPrint.Annotated.Leijen + data ElabWhat = ETypes | EDefns | EAll   deriving (Show, Eq) @@ -66,7 +63,7 @@   , elabFC    :: Maybe FC   , constraintNS :: String        -- ^ filename for adding to constraint variables   , pe_depth  :: Int-+  , noCaseLift :: [Name]         -- ^ types which shouldn't be made arguments to case   -- | We may, recursively, collect transformations to do on the rhs,   -- e.g. rewriting recursive calls to functions defined by 'with'   , rhs_trans :: PTerm -> PTerm@@ -74,10 +71,10 @@   }  toplevel :: ElabInfo-toplevel = EInfo [] emptyContext id [] Nothing "(toplevel)" 0 id (\_ _ _ -> fail "Not implemented")+toplevel = EInfo [] emptyContext id [] Nothing "(toplevel)" 0 [] id (\_ _ _ -> fail "Not implemented")  toplevelWith :: String -> ElabInfo-toplevelWith ns = EInfo [] emptyContext id [] Nothing ns 0 id (\_ _ _ -> fail "Not implemented")+toplevelWith ns = EInfo [] emptyContext id [] Nothing ns 0 [] id (\_ _ _ -> fail "Not implemented")  eInfoNames :: ElabInfo -> [Name] eInfoNames info = map fst (params info) ++ M.keys (inblock info)@@ -91,7 +88,7 @@   , opt_showimp      :: Bool          -- ^ show implicits   , opt_errContext   :: Bool   , opt_repl         :: Bool-  , opt_verbose      :: Bool+  , opt_verbose      :: Int   , opt_nobanner     :: Bool   , opt_quiet        :: Bool   , opt_codegen      :: Codegen@@ -112,6 +109,7 @@   , opt_autoimpls    :: Bool   } deriving (Show, Eq, Generic) +defaultOpts :: IOption defaultOpts = IOption { opt_logLevel   = 0                       , opt_logcats    = []                       , opt_typecase   = False@@ -120,7 +118,7 @@                       , opt_showimp    = False                       , opt_errContext = False                       , opt_repl       = True-                      , opt_verbose    = True+                      , opt_verbose    = 0                       , opt_nobanner   = False                       , opt_quiet      = False                       , opt_codegen    = Via IBCFormat "c"@@ -151,7 +149,8 @@ data Optimisation = PETransform -- ^ partial eval and associated transforms   deriving (Show, Eq, Generic) -defaultOptimise = [PETransform]+defaultOptimise :: [Optimisation]+defaultOptimise = []  -- | Pretty printing options with default verbosity. defaultPPOption :: PPOption@@ -184,7 +183,9 @@ ppOptionIst :: IState -> PPOption ppOptionIst = ppOption . idris_options -data LanguageExt = TypeProviders | ErrorReflection+data LanguageExt = TypeProviders | ErrorReflection | UniquenessTypes+                 | DSLNotation   | ElabReflection  | FCReflection+                 | LinearTypes   deriving (Show, Eq, Read, Ord, Generic)  -- | The output mode in use@@ -204,6 +205,12 @@                      | DefaultCheckingCovering -- ^Total coverage, but may diverge   deriving (Show, Eq, Generic) +-- | Configuration options for interactive editing.+data InteractiveOpts = InteractiveOpts {+    interactiveOpts_indentWith :: Int+  , interactiveOpts_indentClause :: Int+} deriving (Show, Generic)+ -- | The global state used in the Idris monad data IState = IState {     tt_ctxt            :: Context            -- ^ All the currently defined names and their terms@@ -250,6 +257,7 @@   , idris_metavars      :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))]   , idris_coercions              :: [Name]   , idris_errRev                 :: [(Term, Term)]+  , idris_errReduce              :: [Name]   , syntax_rules                 :: SyntaxRules   , syntax_keywords              :: [String]   , imported                     :: [FilePath]                    -- ^ The imported modules@@ -285,14 +293,12 @@   , idris_postulates             :: S.Set Name   , idris_externs                :: S.Set (Name, Int)   , idris_erasureUsed            :: [(Name, Int)]                  -- ^ Function/constructor name, argument position is used-  , idris_whocalls               :: Maybe (M.Map Name [Name])-  , idris_callswho               :: Maybe (M.Map Name [Name])    -- | List of names that were defined in the repl, and can be re-/un-defined   , idris_repl_defs              :: [Name]    -- | Stack of names currently being elaborated, Bool set if it's an-  -- implementation (implementations appear twice; also as a funtion name)+  -- implementation (implementations appear twice; also as a function name)   , elab_stack                   :: [(Name, Bool)]  @@ -304,8 +310,8 @@   , idris_inmodule               :: S.Set Name                -- ^ Names defined in current module   , idris_ttstats                :: M.Map Term (Int, Term)   , idris_fragile                :: Ctxt String               -- ^ Fragile names and explanation.-  }-  deriving Generic+  , idris_interactiveOpts        :: InteractiveOpts+  } deriving Generic  -- Required for parsers library, and therefore trifecta instance Show IState where@@ -330,11 +336,13 @@ deriving instance Binary CGInfo !-} +primDefs :: [Name] primDefs = [ sUN "unsafePerformPrimIO"            , sUN "mkLazyForeignPrim"            , sUN "mkForeignPrim"            , sUN "void"            , sUN "assert_unreachable"+           , sUN "idris_crash"            ]  -- information that needs writing for the current module's .ibc file@@ -366,6 +374,7 @@               | IBCFnInfo Name FnInfo               | IBCTrans Name (Term, Term)               | IBCErrRev (Term, Term)+              | IBCErrReduce Name               | IBCCG Name               | IBCDoc Name               | IBCCoercion Name@@ -387,6 +396,12 @@               | IBCConstraint FC UConstraint   deriving (Show, Generic) +initialInteractiveOpts :: InteractiveOpts+initialInteractiveOpts = InteractiveOpts {+    interactiveOpts_indentWith = 2+  , interactiveOpts_indentClause = 2+}+ -- | The initial state for the compiler idrisInit :: IState idrisInit = IState initContext S.empty []@@ -395,11 +410,11 @@                    emptyContext emptyContext emptyContext emptyContext                    emptyContext emptyContext emptyContext emptyContext                    emptyContext-                   [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []+                   [] [] [] defaultOpts 6 [] [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []                    [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []                    (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty-                   AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []-                   emptyContext S.empty M.empty emptyContext+                   AutomaticWidth S.empty S.empty [] [] [] M.empty [] [] []+                   emptyContext S.empty M.empty emptyContext initialInteractiveOpts   -- | The monad for the main REPL - reading and processing files and@@ -485,6 +500,8 @@          | ColourREPL Bool          | Idemode          | IdemodeSocket+         | IndentWith Int+         | IndentClause Int          | ShowAll          | ShowLibs          | ShowLibDir@@ -506,11 +523,12 @@          | DefaultPartial          | WarnPartial          | WarnReach+         | AuditIPkg          | EvalTypes          | NoCoverage          | ErrContext          | ShowImpl-         | Verbose+         | Verbose Int          | Port REPLPort -- ^ REPL TCP port          | IBCSubDir String          | ImportDir String@@ -597,17 +615,21 @@                    , pparam    :: Bool                    , pscoped   :: Maybe ImplicitInfo -- ^ Nothing, if top level                    , pinsource :: Bool               -- ^ Explicitly written in source+                   , pcount    :: RigCount                    }              | Exp { pargopts :: [ArgOpt]                    , pstatic  :: Static                    , pparam   :: Bool -- ^ this is a param (rather than index)+                   , pcount    :: RigCount                    }              | Constraint { pargopts :: [ArgOpt]-                         ,  pstatic :: Static+                          , pstatic :: Static+                          , pcount    :: RigCount                          }              | TacImp { pargopts :: [ArgOpt]                       , pstatic  :: Static                       , pscript  :: PTerm+                      , pcount    :: RigCount                       }              deriving (Show, Eq, Ord, Data, Generic, Typeable) @@ -616,24 +638,32 @@ !-}  is_scoped :: Plicity -> Maybe ImplicitInfo-is_scoped (Imp _ _ _ s _) = s-is_scoped _               = Nothing+is_scoped (Imp _ _ _ s _ _) = s+is_scoped _                 = Nothing  -- Top level implicit-impl              = Imp [] Dynamic False (Just (Impl False True False)) False+impl              :: Plicity+impl              = Imp [] Dynamic False (Just (Impl False True False)) False RigW -- Machine generated top level implicit-impl_gen          = Imp [] Dynamic False (Just (Impl False True True)) False+impl_gen          :: Plicity+impl_gen          = Imp [] Dynamic False (Just (Impl False True True)) False RigW  -- Scoped implicits-forall_imp        = Imp [] Dynamic False (Just (Impl False False True)) False-forall_constraint = Imp [] Dynamic False (Just (Impl True False True)) False+forall_imp        :: Plicity+forall_imp        = Imp [] Dynamic False (Just (Impl False False True)) False RigW+forall_constraint :: Plicity+forall_constraint = Imp [] Dynamic False (Just (Impl True False True)) False RigW -expl              = Exp [] Dynamic False-expl_param        = Exp [] Dynamic True+expl              :: Plicity+expl              = Exp [] Dynamic False RigW+expl_param        :: Plicity+expl_param        = Exp [] Dynamic True RigW -constraint        = Constraint [] Static+constraint        :: Plicity+constraint        = Constraint [] Static RigW -tacimpl t         = TacImp [] Dynamic t+tacimpl           :: PTerm -> Plicity+tacimpl t         = TacImp [] Dynamic t RigW  data FnOpt = Inlinable -- ^ always evaluate when simplifying            | TotalFn | PartialFn | CoveringFn@@ -649,14 +679,9 @@            | CExport String                 -- ^ export, with a C name            | ErrorHandler                   -- ^ an error handler for use with the ErrorReflection extension            | ErrorReverse                   -- ^ attempt to reverse normalise before showing in error+           | ErrorReduce                    -- ^ unfold definition before showing an error            | Reflection                     -- ^ a reflecting function, compile-time only            | Specialise [(Name, Maybe Int)] -- ^ specialise it, freeze these names-           | UnfoldIface Name [Name]-                  -- ^ Unfold given interface name in the definition, the-                  -- top level methods, and anything which has-                  -- the interface name as an argument. This is to unfold-                  -- things for termination checking, as interfaces will otherwise-                  -- cause problems            | Constructor -- ^ Data constructor type            | AutoHint    -- ^ use in auto implicit search            | PEGenerated -- ^ generated by partial evaluator@@ -1403,7 +1428,7 @@ -- Interface data  data InterfaceInfo = CI {-    implementationCtorName                   :: Name+    implementationCtorName             :: Name   , interface_methods                  :: [(Name, (Bool, FnOpts, PTerm))] -- ^ flag whether it's a "data" method   , interface_defaults                 :: [(Name, (Name, PDecl))]         -- ^ method name -> default impl   , interface_default_super_interfaces :: [PDecl]@@ -1617,8 +1642,8 @@ getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)  getInferType (Bind n b sc)  = Bind n (toTy b) $ getInferType sc-  where toTy (Lam t)        = Pi Nothing t (TType (UVar [] 0))-        toTy (PVar t)       = PVTy t+  where toTy (Lam r t)      = Pi r Nothing t (TType (UVar [] 0))+        toTy (PVar _ t)     = PVTy t         toTy b              = b getInferType (App _ (App _ _ ty) _) = ty @@ -1813,7 +1838,15 @@       depth d . bracket p startPrec . group . align $       kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>       kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)-    prettySe d p bnd (PPi (Exp l s _) n _ ty sc)+    prettySe d p bnd (PPi (Exp l s _ rig) n _ ty sc)+      | Rig0 <- rig =+          depth d . bracket p startPrec . group $+          enclose lparen rparen (group . align $ text "0" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>+          st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc+      | Rig1 <- rig =+          depth d . bracket p startPrec . group $+          enclose lparen rparen (group . align $ text "1" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>+          st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc       | n `elem` allNamesIn sc || ppopt_impl ppo && uname n || n `elem` docArgs           || ppopt_pinames ppo && uname n =           depth d . bracket p startPrec . group $@@ -1833,24 +1866,28 @@           case s of             Static -> text "%static" <> space             _      -> empty-    prettySe d p bnd (PPi (Imp l s _ fa _) n _ ty sc)+    prettySe d p bnd (PPi (Imp l s _ fa _ rig) n _ ty sc)       | ppopt_impl ppo =           depth d . bracket p startPrec $-          lbrace <> prettyBindingOf n True <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>+          lbrace <> showRig rig n <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>           st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc       | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc       where+        showRig Rig0 n = text "0" <+> prettyBindingOf n True+        showRig Rig1 n = text "1" <+> prettyBindingOf n True+        showRig _ n = prettyBindingOf n True+         st =           case s of             Static -> text "%static" <> space             _      -> empty-    prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =+    prettySe d p bnd (PPi (Constraint _ _ rig) n _ ty sc) =       depth d . bracket p startPrec $       prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc-    prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch{}])) n _ ty sc) =+    prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch{}]) rig) n _ ty sc) =       lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>       rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc-    prettySe d p bnd (PPi (TacImp _ _ s) n _ ty sc) =+    prettySe d p bnd (PPi (TacImp _ _ s rig) n _ ty sc) =       depth d . bracket p startPrec $       lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>       rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc@@ -2250,7 +2287,7 @@  getShowArgs :: [PArg] -> [PArg] getShowArgs [] = []-getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs+getShowArgs (e@(PExp _ _ _ _) : xs) = e : getShowArgs xs getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs                      | PImp _ _ _ _ tm <- e                      , containsHole tm = e : getShowArgs xs@@ -2378,7 +2415,7 @@     ni i env (PUnquote tm)        = ni (i - 1) env tm     ni i env tm                   = concatMap (ni i env) (children tm) -    niTacImp i env (TacImp _ _ scr) = ni i env scr+    niTacImp i env (TacImp _ _ scr _) = ni i env scr     niTacImp _ _ _                  = []  @@ -2414,7 +2451,7 @@     niTms i set []        = set     niTms i set (x : xs)  = niTms i (ni i set x) xs -    niTacImp i set (TacImp _ _ scr) = ni i set scr+    niTacImp i set (TacImp _ _ scr _) = ni i set scr     niTacImp i set _                = set  -- Return names which are valid implicits in the given term (type).@@ -2470,6 +2507,8 @@     ni 0 env (PIfThenElse _ c t f)            = mapM_ (ni 0 env) [c, t, f]     ni 0 env (PLam fc n _ ty sc)              = do ni 0 env ty; ni 0 (n:env) sc     ni 0 env (PPi p n _ ty sc)                = do ni 0 env ty; ni 0 (n:env) sc+    ni 0 env (PLet fc n _ ty val sc)          = do ni 0 env ty;+                                                   ni 0 env val; ni 0 (n:env) sc     ni 0 env (PRewrite _ _ l r _)             = do ni 0 env l; ni 0 env r     ni 0 env (PTyped l r)                     = do ni 0 env l; ni 0 env r     ni 0 env (PPair _ _ _ l r)                = do ni 0 env l; ni 0 env r@@ -2523,7 +2562,7 @@      ni i env tm                     = concatMap (ni i env) (children tm) -    niTacImp i env (TacImp _ _ scr) = ni i env scr+    niTacImp i env (TacImp _ _ scr _) = ni i env scr     niTacImp _ _ _                  = []  -- Return which of the given names are used in the given term.@@ -2558,12 +2597,12 @@      ni i env tm                     = concatMap (ni i env) (children tm) -    niTacImp i env (TacImp _ _ scr) = ni i env scr+    niTacImp i env (TacImp _ _ scr _) = ni i env scr     niTacImp _ _ _                = []  -- Return the list of inaccessible (= dotted) positions for a name. getErasureInfo :: IState -> Name -> [Int] getErasureInfo ist n =     case lookupCtxtExact n (idris_optimisation ist) of-        Just (Optimise inacc detag force) -> map fst inacc+        Just (Optimise inacc _ _) -> map fst inacc         Nothing -> []

@@ -72,8 +72,8 @@   isApropos str (CaseOp _ ty ty' _ _ _) = isApropos str ty  instance Apropos (Binder (TT Name)) where-  isApropos str (Lam ty)      = str == T.pack "\\" || isApropos str ty-  isApropos str (Pi _ ty _)   = str == T.pack "->" || isApropos str ty+  isApropos str (Lam _ ty)    = str == T.pack "\\" || isApropos str ty+  isApropos str (Pi _ _ ty _) = str == T.pack "->" || isApropos str ty   isApropos str (Let ty val)  = str == T.pack "let" || isApropos str ty || isApropos str val   isApropos str (NLet ty val) = str == T.pack "let" || isApropos str ty || isApropos str val   isApropos str _             = False -- these shouldn't occur in defined libraries

@@ -15,8 +15,8 @@ Finally, merge the generated patterns with the original, by matching. Always take the "more specific" argument when there is a discrepancy, i.e. names over '_', patterns over names, etc.- -}+ {-# LANGUAGE PatternGuards #-}  module Idris.CaseSplit(@@ -28,10 +28,8 @@   ) where  import Idris.AbsSyntax-import Idris.AbsSyntaxTree (IState, Idris, PTerm) import Idris.Core.Evaluate import Idris.Core.TT-import Idris.Core.Typecheck import Idris.Delaborate import Idris.Elab.Term import Idris.Elab.Value@@ -39,18 +37,11 @@ import Idris.Error import Idris.Output import Idris.Parser-import Idris.Parser.Helpers  import Control.Monad import Control.Monad.State.Strict import Data.Char import Data.List (isPrefixOf, isSuffixOf)-import Data.Maybe-import Debug.Trace-import Text.Parser.Char (anyChar)-import Text.Parser.Combinators-import Text.Trifecta (Result(..), parseString)-import Text.Trifecta.Delta  -- | Given a variable to split, and a term application, return a list -- of variable updates, paired with a flag to say whether the given@@ -109,11 +100,11 @@                        explicit :: [Name],                        updates :: [(Name, PTerm)] } -addUpdate :: Name -> Idris.AbsSyntaxTree.PTerm -> State MergeState ()+addUpdate :: Name -> PTerm -> State MergeState () addUpdate n tm = do ms <- get                     put (ms { updates = ((n, stripNS tm) : updates ms) } ) -inventName :: Idris.AbsSyntaxTree.IState -> Maybe Name -> Name -> State MergeState Name+inventName :: IState -> Maybe Name -> Name -> State MergeState Name inventName ist ty n =     do ms <- get        let supp = case ty of@@ -142,7 +133,7 @@ varlist :: [Name] varlist = map (sUN . (:[])) "xyzwstuv" -- EB's personal preference :) -stripNS :: Idris.AbsSyntaxTree.PTerm -> Idris.AbsSyntaxTree.PTerm+stripNS :: PTerm -> PTerm stripNS tm = mapPT dens tm where     dens (PRef fc hls n) = PRef fc hls (nsroot n)     dens t = t@@ -212,7 +203,7 @@            [ty] -> let ty' = normalise (tt_ctxt ist) [] ty in                        map (tyName . snd) (getArgTys ty') ++ repeat Nothing            _ -> repeat Nothing-  where tyName (Bind _ (Pi _ _ _) _) = Just (sUN "->")+  where tyName (Bind _ (Pi _ _ _ _) _) = Just (sUN "->")         tyName t | (P _ d _, [_, ty]) <- unApply t,                    d == sUN "Delayed" = tyName ty                  | (P _ n _, _) <- unApply t = Just n@@ -395,27 +386,29 @@           -> Name     -- ^ User given name           -> FilePath -- ^ Source file name           -> Idris String-getClause l fn un fp+getClause l _ un fp     = do i <- getIState+         indentClause <- getIndentClause+--         runIO . traceIO $ "indentClause = " ++ show indentClause          case lookupCtxt un (idris_interfaces i) of-              [c] -> return (mkInterfaceBodies i (interface_methods c))+              [c] -> return (mkInterfaceBodies indentClause i (interface_methods c))               _ -> do ty_in <- getInternalApp fp l                       let ty = case ty_in of-                                    PTyped n t -> t+                                    PTyped _ t -> t                                     x -> x                       ist <- get-                      let ap = mkApp ist ty []-                      return (showLHSName un ++ " " ++ ap ++ "= ?"+                      let app = mkApp ist ty []+                      return (showLHSName un ++ " " ++ app ++ "= ?"                                       ++ showRHSName un ++ "_rhs")    where mkApp :: IState -> PTerm -> [Name] -> String-         mkApp i (PPi (Exp _ _ False) (MN _ _) _ ty sc) used+         mkApp i (PPi (Exp _ _ False _) (MN _ _) _ ty sc) used                = let n = getNameFrom i used ty in                      show n ++ " " ++ mkApp i sc (n : used)-         mkApp i (PPi (Exp _ _ False) (UN n) _ ty sc) used+         mkApp i (PPi (Exp _ _ False _) (UN n) _ ty sc) used             | thead n == '_'                = let n = getNameFrom i used ty in                      show n ++ " " ++ mkApp i sc (n : used)-         mkApp i (PPi (Exp _ _ False) n _ _ sc) used+         mkApp i (PPi (Exp _ _ False _) n _ _ sc) used                = show n ++ " " ++ mkApp i sc (n : used)          mkApp i (PPi _ _ _ _ sc) used = mkApp i sc used          mkApp i _ _ = ""@@ -431,11 +424,11 @@          getNameFrom i used _ = uniqueNameFrom (mkSupply [sUN "x", sUN "y",                                                           sUN "z"]) used -         -- write method declarations, indent with 4 spaces-         mkInterfaceBodies :: IState -> [(Name, (Bool, FnOpts, PTerm))] -> String-         mkInterfaceBodies i ns+         -- write method declarations, indent with `indent` spaces.+         mkInterfaceBodies :: Int -> IState -> [(Name, (Bool, FnOpts, PTerm))] -> String+         mkInterfaceBodies indent i ns              = showSep "\n"-                  (zipWith (\(n, (_, _, ty)) m -> "    " +++                  (zipWith (\(n, (_, _, ty)) m -> replicate indent ' ' ++                             def (show (nsroot n)) ++ " "                                  ++ mkApp i ty []                                  ++ "= ?"@@ -460,9 +453,9 @@ -- Purely syntactic - turn a pattern match clause into a with and a new -- match clause -mkWith :: String -> Name -> String-mkWith str n = let str' = replaceRHS str "with (_)"-               in str' ++ "\n" ++ newpat str+mkWith :: String -> Name -> Int -> String+mkWith str n indent = let str' = replaceRHS str "with (_)"+                      in str' ++ "\n" ++ newpat str     where replaceRHS [] str = str          replaceRHS ('?':'=': rest) str = str@@ -471,8 +464,7 @@          replaceRHS (x : rest) str = x : replaceRHS rest str           newpat ('>':patstr) = '>':newpat patstr-         newpat patstr =-           "  " +++         newpat patstr = replicate indent ' ' ++            replaceRHS patstr "| with_pat = ?" ++ showRHSName n ++ "_rhs"  -- Replace _ with names in missing clauses

@@ -5,7 +5,9 @@ License     : BSD3 Maintainer  : The Idris Community. -}+ {-# LANGUAGE Arrows #-}+ module Idris.CmdOptions   (     module Idris.CmdOptions@@ -19,7 +21,6 @@                         getPort, opt) import Idris.AbsSyntaxTree import Idris.Info (getIdrisVersion)--- import Idris.REPL import IRTS.CodegenCommon  import Control.Monad.Trans (lift)@@ -33,8 +34,10 @@ import Options.Applicative import Options.Applicative.Arrows import Options.Applicative.Types (ReadM(..))-import Safe (lastMay)+ import Text.ParserCombinators.ReadP hiding (many, option)++import Safe (lastMay) import qualified Text.PrettyPrint.ANSI.Leijen as PP  runArgParser :: IO [Opt]@@ -97,14 +100,15 @@   <|> flag' Idemode       (long "ide-mode"        <> help "Run the Idris REPL with machine-readable syntax")   <|> flag' IdemodeSocket (long "ide-mode-socket" <> help "Choose a socket for IDE mode to listen on") -  <|> (Client <$> strOption (long "client"))+  -- Client flags+  <|> Client <$> strOption (long "client")    -- Logging Flags-  <|> (OLogging <$> option auto (long "log" <> metavar "LEVEL" <> help "Debugging log level"))-  <|> (OLogCats <$> option (str >>= parseLogCats)+  <|> OLogging <$> option auto (long "log" <> metavar "LEVEL" <> help "Debugging log level")+  <|> OLogCats <$> option (str >>= parseLogCats)                            (long "logging-categories"                          <> metavar "CATS"-                         <> help "Colon separated logging categories. Use --listlogcats to see list."))+                         <> help "Colon separated logging categories. Use --listlogcats to see list.")    -- Turn off things   <|> flag' NoBasePkgs (long "nobasepkgs" <> help "Do not use the given base package")@@ -113,7 +117,7 @@    <|> flag' NoREPL     (long "check"      <> help "Typecheck only, don't start the REPL") -  <|> (Output <$> strOption (short 'o' <> long "output" <> metavar "FILE" <> help "Specify output file"))+  <|> Output <$> strOption (short 'o' <> long "output" <> metavar "FILE" <> help "Specify output file")    --   <|> flag' TypeCase (long "typecase")   <|> flag' Interface      (long "interface"   <> help "Generate interface files from ExportLists")@@ -122,6 +126,7 @@   <|> flag' DefaultPartial (long "partial")   <|> flag' WarnPartial    (long "warnpartial" <> help "Warn about undeclared partial functions")   <|> flag' WarnReach      (long "warnreach"   <> help "Warn about reachable but inaccessible arguments")+  <|> flag' AuditIPkg      (long "warnipkg"    <> help "Warn about possible incorrect package specifications")   <|> flag' NoCoverage     (long "nocoverage")   <|> flag' ErrContext     (long "errorcontext") @@ -134,35 +139,45 @@   <|> flag' ShowDocDir      (long "docdir"      <> help "Display idrisdoc install directory")   <|> flag' ShowIncs        (long "include"     <> help "Display the includes flags") -  <|> flag' Verbose (short 'V' <> long "verbose" <> help "Loud verbosity")+  <|> flag' (Verbose 3) (long "V2" <> help "Loudest verbosity")+  <|> flag' (Verbose 2) (long "V1" <> help "Louder verbosity")+  <|> flag' (Verbose 1) (short 'V' <> long "V0" <>long "verbose" <> help "Loud verbosity") -  <|> (IBCSubDir <$> strOption (long "ibcsubdir" <> metavar "FILE" <> help "Write IBC files into sub directory"))-  <|> (ImportDir <$> strOption (short 'i' <> long "idrispath" <> help "Add directory to the list of import paths"))-  <|> (SourceDir <$> strOption (long "sourcepath" <> help "Add directory to the list of source search paths"))+  <|> IBCSubDir <$> strOption (long "ibcsubdir" <> metavar "FILE" <> help "Write IBC files into sub directory")+  <|> ImportDir <$> strOption (short 'i' <> long "idrispath" <> help "Add directory to the list of import paths")+  <|> SourceDir <$> strOption (long "sourcepath" <> help "Add directory to the list of source search paths")    <|> flag' WarnOnly (long "warn") -  <|> (Pkg  <$> strOption (short 'p' <> long "package" <> help "Add package as a dependency"))-  <|> (Port <$> option portReader (long "port" <> metavar "PORT" <> help "REPL TCP port - pass \"none\" to not bind any port"))+  <|> Pkg  <$> strOption (short 'p' <> long "package" <> help "Add package as a dependency")+  <|> Port <$> option portReader (long "port" <> metavar "PORT" <> help "REPL TCP port - pass \"none\" to not bind any port")    -- Package commands-  <|> (PkgBuild      <$> strOption (long "build"      <> metavar "IPKG" <> help "Build package"))-  <|> (PkgInstall    <$> strOption (long "install"    <> metavar "IPKG" <> help "Install package"))-  <|> (PkgREPL       <$> strOption (long "repl"       <> metavar "IPKG" <> help "Launch REPL, only for executables"))-  <|> (PkgClean      <$> strOption (long "clean"      <> metavar "IPKG" <> help "Clean package"))+  <|> PkgBuild   <$> strOption (long "build"    <> metavar "IPKG" <> help "Build package")+  <|> PkgInstall <$> strOption (long "install"  <> metavar "IPKG" <> help "Install package")+  <|> PkgREPL    <$> strOption (long "repl"     <> metavar "IPKG" <> help "Launch REPL, only for executables")+  <|> PkgClean   <$> strOption (long "clean"    <> metavar "IPKG" <> help "Clean package")   <|> (PkgDocBuild   <$> strOption (long "mkdoc"      <> metavar "IPKG" <> help "Generate IdrisDoc for package"))-  <|> (PkgDocInstall <$> strOption (long "installdoc" <> metavar "IPKG" <> help "Install IdrisDoc for package"))-  <|> (PkgCheck      <$> strOption (long "checkpkg"   <> metavar "IPKG" <> help "Check package only"))-  <|> (PkgTest       <$> strOption (long "testpkg"    <> metavar "IPKG" <> help "Run tests for package"))+  <|> PkgDocInstall <$> strOption (long "installdoc" <> metavar "IPKG" <> help "Install IdrisDoc for package")+  <|> PkgCheck   <$> strOption (long "checkpkg" <> metavar "IPKG" <> help "Check package only")+  <|> PkgTest    <$> strOption (long "testpkg"  <> metavar "IPKG" <> help "Run tests for package") +  -- Interactive Editing Flags+  <|> IndentWith    <$> option auto (long "indent-with"+                                           <> metavar "INDENT"+                                           <> help "Indentation to use with :makewith (default 2)")+  <|> IndentClause  <$> option auto (long "indent-clause"+                                           <> metavar "INDENT"+                                           <> help "Indentation to use with :addclause (default 2)")+   -- Misc options-  <|> (BCAsm <$> strOption (long "bytecode"))+  <|> BCAsm <$> strOption (long "bytecode")    <|> flag' (OutputTy Raw)          (short 'S' <> long "codegenonly" <> help "Do no further compilation of code generator output")   <|> flag' (OutputTy Object)       (short 'c' <> long "compileonly" <> help "Compile to object files rather than an executable") -  <|> (DumpDefun <$> strOption (long "dumpdefuns"))-  <|> (DumpCases <$> strOption (long "dumpcases"))+  <|> DumpDefun <$> strOption (long "dumpdefuns")+  <|> DumpCases <$> strOption (long "dumpcases")    <|> (UseCodegen . parseCodegen) <$> strOption (long "codegen"                                               <> metavar "TARGET"@@ -172,14 +187,17 @@                                                  <> metavar "TARGET"                                                  <> help "Pass the name of the code generator. This option is for codegens that take JSON formatted IR.")) -  <|> (CodegenArgs <$> strOption (long "cg-opt"-                               <> metavar "ARG"-                               <> help "Arguments to pass to code generator"))+  <|> CodegenArgs <$> strOption (long "cg-opt"+                                 <> metavar "ARG"+                                 <> help "Arguments to pass to code generator") -  <|> (EvalExpr <$> strOption (long "eval" <> short 'e' <> metavar "EXPR" <> help "Evaluate an expression without loading the REPL"))+  <|> EvalExpr <$> strOption (long "eval"+                              <> short 'e'+                              <> metavar "EXPR"+                              <> help "Evaluate an expression without loading the REPL")    <|> flag' (InterpretScript "Main.main") (long "execute" <> help "Execute as idris")-  <|> (InterpretScript <$> strOption      (long "exec" <> metavar "EXPR" <> help "Execute as idris"))+  <|> InterpretScript <$> strOption      (long "exec" <> metavar "EXPR" <> help "Execute as idris")    <|> ((Extension . getExt) <$> strOption (long "extension"                                         <> short 'X'@@ -195,10 +213,10 @@   <|> flag' (AddOpt PETransform) (long "partial-eval")   <|> flag' (RemoveOpt PETransform) (long "no-partial-eval" <> help "Switch off partial evaluation, mainly for debugging purposes") -  <|> (OptLevel <$> option auto (short 'O' <> long "level"))+  <|> OptLevel <$> option auto (short 'O' <> long "level") -  <|> (TargetTriple <$> strOption (long "target" <> metavar "TRIPLE" <> help "If supported the codegen will target the named triple."))-  <|> (TargetCPU    <$> strOption (long "cpu"    <> metavar "CPU"    <> help "If supported the codegen will target the named CPU e.g. corei7 or cortex-m3"))+  <|> TargetTriple <$> strOption (long "target" <> metavar "TRIPLE" <> help "If supported the codegen will target the named triple.")+  <|> TargetCPU    <$> strOption (long "cpu"    <> metavar "CPU"    <> help "If supported the codegen will target the named CPU e.g. corei7 or cortex-m3")    -- Colour Options   <|> flag' (ColourREPL True)  (long "colour"   <> long "color"   <> help "Force coloured output")

@@ -159,6 +159,7 @@ completeCmd :: String -> CompletionFunc Idris completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookupInHelp cmd     where completeArg FileArg = completeFilename (prev, next)+          completeArg ShellCommandArg = completeFilename (prev, next)           completeArg NameArg = completeName UpTo [] (prev, next)           completeArg OptionArg = completeOption (prev, next)           completeArg ModuleArg = noCompletion (prev, next)

@@ -490,6 +490,19 @@                            return (RUType x1)                    _ -> error "Corrupted binary data for Raw" +instance Binary RigCount where+        put x = case x of+                     Rig0 -> putWord8 0+                     Rig1 -> putWord8 1+                     RigW -> putWord8 2+        get = do i <- getWord8+                 case i of+                     0 -> return Rig0+                     1 -> return Rig1+                     2 -> return RigW+                     _ -> error "Corrupted binary data for RigCount"++ instance Binary ImplicitInfo where         put x           = case x of@@ -502,12 +515,14 @@ instance (Binary b) => Binary (Binder b) where         put x           = case x of-                Lam x1 -> do putWord8 0-                             put x1-                Pi x1 x2 x3 -> do putWord8 1-                                  put x1-                                  put x2-                                  put x3+                Lam x1 x2 -> do putWord8 0+                                put x1+                                put x2+                Pi x1 x2 x3 x4 -> do putWord8 1+                                     put x1+                                     put x2+                                     put x3+                                     put x4                 Let x1 x2 -> do putWord8 2                                 put x1                                 put x2@@ -523,19 +538,22 @@                 Guess x1 x2 -> do putWord8 6                                   put x1                                   put x2-                PVar x1 -> do putWord8 7-                              put x1+                PVar x1 x2 -> do putWord8 7+                                 put x1+                                 put x2                 PVTy x1 -> do putWord8 8                               put x1         get           = do i <- getWord8                case i of                    0 -> do x1 <- get-                           return (Lam x1)+                           x2 <- get+                           return (Lam x1 x2)                    1 -> do x1 <- get                            x2 <- get                            x3 <- get-                           return (Pi x1 x2 x3)+                           x4 <- get+                           return (Pi x1 x2 x3 x4)                    2 -> do x1 <- get                            x2 <- get                            return (Let x1 x2)@@ -552,7 +570,8 @@                            x2 <- get                            return (Guess x1 x2)                    7 -> do x1 <- get-                           return (PVar x1)+                           x2 <- get+                           return (PVar x1 x2)                    8 -> do x1 <- get                            return (PVTy x1)                    _ -> error "Corrupted binary data for Binder"

@@ -174,7 +174,7 @@                   then S.empty                   else if n `elem` ps                           then S.union (nut ps f) (nut ps a)-                          else S.insert (n, map argNames args) +                          else S.insert (n, map argNames args)                                    (S.unions $ map (nut ps) args)         | (P (TCon _ _) n _, _) <- unApply fn = S.empty         | otherwise = S.union (nut ps f) (nut ps a)@@ -245,7 +245,7 @@ runCaseBuilder ei bld = runState $ runReaderT bld ei  data Phase = CoverageCheck [Int] -- list of positions explicitly given-           | CompileTime +           | CompileTime            | RunTime     deriving (Show, Eq) @@ -253,7 +253,7 @@ -- Work Right to Left  simpleCase :: Bool -> SC -> Bool ->-              Phase -> FC -> +              Phase -> FC ->               -- Following two can be empty lists when Phase = CoverageCheck               [Int] -> -- Inaccessible argument positions               [(Type, Bool)] -> -- (Argument type, whether it's canonical)@@ -392,7 +392,7 @@     toPat' [] (Constant x) | isTypeConst x = PTyPat                            | otherwise     = PConst x -    toPat' [] (Bind n (Pi _ t _) sc)+    toPat' [] (Bind n (Pi _ _ t _) sc)         | reflect && noOccurrence n sc         = PReflected (sUN "->") [toPat' [] t, toPat' [] sc] @@ -444,7 +444,7 @@ -- order CompileTime ns cs _ = (map fst ns, cs) order _ []  cs cans = ([], cs) order _ ns' [] cans = (map fst ns', [])-order (CoverageCheck pos) ns' cs cans +order (CoverageCheck pos) ns' cs cans     = let ns_out = pick 0 [] (map fst ns')           cs_out = map pickClause cs in           (ns_out, cs_out)@@ -454,7 +454,7 @@     -- Order the list so that things in a position in 'pos' are in the first     -- part, then all the other things later. Otherwise preserve order.     pick i skipped [] = reverse skipped-    pick i skipped (x : xs) +    pick i skipped (x : xs)          | i `elem` pos = x : pick (i + 1) skipped xs          | otherwise    = pick (i + 1) (x : skipped) xs @@ -823,7 +823,7 @@ prune _ t = t  stripLambdas :: CaseDef -> CaseDef-stripLambdas (CaseDef ns (STerm (Bind x (Lam _) sc)) tm)+stripLambdas (CaseDef ns (STerm (Bind x (Lam _ _) sc)) tm)     = stripLambdas (CaseDef (ns ++ [x]) (STerm (instantiate (P Bound x Erased) sc)) tm) stripLambdas x = x 

@@ -1,3 +1,4 @@+{-# LANGUAGE FlexibleContexts, MultiParamTypeClasses #-} {-| Module      : Idris.Core.Constraints Description : Check universe constraints.

@@ -40,6 +40,7 @@ instance NFData Err instance NFData ErrorReportPart instance NFData ImplicitInfo+instance NFData RigCount instance (NFData b) => NFData (Binder b) instance NFData UExp instance NFData NameType

@@ -99,7 +99,7 @@ setNextName = do env <- get_env                  ES (p, a) s e <- get                  let pargs = map fst (getArgTys (ptype p))-                 initNextNameFrom (pargs ++ map fst env)+                 initNextNameFrom (pargs ++ map fstEnv env)  initNextNameFrom :: [Name] -> Elab' aux () initNextNameFrom ns = do ES (p, a) s e <- get@@ -327,7 +327,7 @@         isInj ctxt (App _ f a) = isInj ctxt f         isInj ctxt (Constant _) = True         isInj ctxt (TType _) = True-        isInj ctxt (Bind _ (Pi _ _ _) sc) = True+        isInj ctxt (Bind _ (Pi _ _ _ _) sc) = True         isInj ctxt _ = False  -- | get implementation argument names@@ -441,8 +441,8 @@ introTy :: Raw -> Maybe Name -> Elab' aux () introTy ty n = processTactic' (IntroTy ty n) -forall :: Name -> Maybe ImplicitInfo -> Raw -> Elab' aux ()-forall n i t = processTactic' (Forall n i t)+forall :: Name -> RigCount -> Maybe ImplicitInfo -> Raw -> Elab' aux ()+forall n r i t = processTactic' (Forall n r i t)  letbind :: Name -> Raw -> Raw -> Elab' aux () letbind n t v = processTactic' (LetBind n t v)@@ -463,18 +463,17 @@ equiv tm = processTactic' (Equiv tm)  -- | Turn the current hole into a pattern variable with the provided--- name, made unique if MN+-- name, made unique if not the same as the head of the hole queue patvar :: Name -> Elab' aux () patvar n@(SN _) = do apply (Var n) []; solve patvar n = do env <- get_env               hs <- get_holes-              if (n `elem` map fst env) then do apply (Var n) []; solve-                else do n' <- case n of-                                    UN _ -> return $! n-                                    MN _ _ -> unique_hole n-                                    NS _ _ -> return $! n-                                    x -> return $! n-                        processTactic' (PatVar n')+              if (n `elem` map fstEnv env) then do apply (Var n) []; solve+                else do n' <- case hs of+                                   (h : hs) -> if n == h then return n+                                                  else unique_hole n+                                   _ -> unique_hole n+                        processTactic' (PatVar n)  -- | Turn the current hole into a pattern variable with the provided -- name, but don't make MNs unique.@@ -482,11 +481,11 @@ patvar' n@(SN _) = do apply (Var n) [] ; solve patvar' n = do env <- get_env                hs <- get_holes-               if (n `elem` map fst env) then do apply (Var n) [] ; solve+               if (n `elem` map fstEnv env) then do apply (Var n) [] ; solve                   else processTactic' (PatVar n) -patbind :: Name -> Elab' aux ()-patbind n = processTactic' (PatBind n)+patbind :: Name -> RigCount -> Elab' aux ()+patbind n r = processTactic' (PatBind n r)  focus :: Name -> Elab' aux () focus n = processTactic' (Focus n)@@ -579,9 +578,9 @@        -- Count arguments to check if we need to normalise the type        let usety = if argsOK (finalise ty) imps                       then finalise ty-                      else whnfArgs ctxt env (finalise ty)+                      else normalise ctxt env (finalise ty)        claims <- -- trace (show (fn, imps, ty, map fst env, normalise ctxt env (finalise ty))) $-                 mkClaims usety imps [] (map fst env)+                 mkClaims usety imps [] (map fstEnv env)        ES (p, a) s prev <- get        -- reverse the claims we made so that args go left to right        let n = length (filter not imps)@@ -590,7 +589,7 @@        return $! claims   where     argsOK :: Type -> [a] -> Bool-    argsOK (Bind n (Pi _ _ _) sc) (i : is) = argsOK sc is+    argsOK (Bind n (Pi _ _ _ _) sc) (i : is) = argsOK sc is     argsOK _ (i : is) = False     argsOK _ [] = True @@ -599,13 +598,13 @@              -> [(Name, Name)] -- ^ Accumulator for produced claims              -> [Name] -- ^ Hypotheses              -> Elab' aux [(Name, Name)] -- ^ The names of the arguments and their holes, resp.-    mkClaims (Bind n' (Pi _ t_in _) sc) (i : is) claims hs =+    mkClaims (Bind n' (Pi _ _ t_in _) sc) (i : is) claims hs =         do let t = rebind hs t_in            n <- getNameFrom (mkMN n') --            when (null claims) (start_unify n)            let sc' = instantiate (P Bound n t) sc            env <- get_env-           claim n (forgetEnv (map fst env) t)+           claim n (forgetEnv (map fstEnv env) t)            when i (movelast n)            mkClaims sc' is ((n', n) : claims) hs     mkClaims t [] claims _ = return $! (reverse claims)@@ -713,7 +712,7 @@     priOrder _ Nothing = GT     priOrder (Just (x, _)) (Just (y, _)) = compare x y -    doClaims (Bind n' (Pi _ t _) sc) (i : is) claims =+    doClaims (Bind n' (Pi _ _ t _) sc) (i : is) claims =         do n <- unique_hole (mkMN n')            when (null claims) (start_unify n)            let sc' = instantiate (P Bound n t) sc@@ -749,14 +748,14 @@             = do g <- goal                  ctxt <- get_context                  env <- get_env-                 case (whnf ctxt env g) of-                    Bind _ (Pi _ _ _) _ -> return ()+                 case (normalise ctxt env g) of+                    Bind _ (Pi _ _ _ _) _ -> return ()                     _ -> do a <- getNameFrom (sMN 0 "__pargTy")                             b <- getNameFrom (sMN 0 "__pretTy")                             f <- getNameFrom (sMN 0 "pf")                             claim a RType                             claim b RType-                            claim f (RBind n (Pi Nothing (Var a) RType) (Var b))+                            claim f (RBind n (Pi RigW Nothing (Var a) RType) (Var b))                             movelast a                             movelast b                             fill (Var f)@@ -776,7 +775,7 @@        s <- getNameFrom (sMN 0 "is")        claim a RType        claim b RType-       claim f (RBind (sMN 0 "_aX") (Pi Nothing (Var a) RType) (Var b))+       claim f (RBind (sMN 0 "_aX") (Pi RigW Nothing (Var a) RType) (Var b))        tm <- get_term        start_unify s        -- if 'infer' is set, we're assuming it's a simply typed application@@ -824,10 +823,10 @@        focus s; attack;        ctxt <- get_context        env <- get_env-       case whnf ctxt env fty of+       case normalise ctxt env fty of             -- if f gives a function type, unify our argument type with             -- f's expected argument type-            Bind _ (Pi _ argty _) _ -> unifyGoal (forget argty)+            Bind _ (Pi _ _ argty _) _ -> unifyGoal (forget argty)             -- Can't infer a type for 'f', so fail here (and drop back to             -- simply typed application where we infer the type for f)             _ -> fail "Can't make type"@@ -846,11 +845,11 @@  -- Abstract over an argument of unknown type, giving a name for the hole -- which we'll fill with the argument type too.-arg :: Name -> Maybe ImplicitInfo -> Name -> Elab' aux ()-arg n i tyhole = do ty <- unique_hole tyhole-                    claim ty RType-                    movelast ty-                    forall n i (Var ty)+arg :: Name -> RigCount -> Maybe ImplicitInfo -> Name -> Elab' aux ()+arg n r i tyhole = do ty <- unique_hole tyhole+                      claim ty RType+                      movelast ty+                      forall n r i (Var ty)  -- try a tactic, if it adds any unification problem, return an error no_errors :: Elab' aux () -> Maybe Err -> Elab' aux ()@@ -870,7 +869,7 @@                case reverse ps' of                     ((x, y, _, env, inerr, while, _) : _) ->                        let (xp, yp) = getProvenance inerr-                           env' = map (\(x, b) -> (x, binderTy b)) env in+                           env' = map (\(x, rig, b) -> (x, binderTy b)) env in                                   lift $ tfail $                                          case err of                                               Nothing -> CantUnify False (x, xp) (y, yp) inerr env' 0@@ -1014,7 +1013,7 @@         getHoleInfo h = do focus h                            g <- goal                            env <- get_env-                           return (h, g, env)+                           return (h, g, envBinders env)  qshow :: Fails -> String qshow fs = show (map (\ (x, y, _, _, _, _, _) -> (x, y)) fs)

@@ -14,18 +14,21 @@                 rt_simplify, simplify, inlineSmall,                 specialise, unfold, convEq, convEq',                 Def(..), CaseInfo(..), CaseDefs(..),-                Accessibility(..), Injectivity, Totality(..), PReason(..), MetaInformation(..),+                Accessibility(..), Injectivity, Totality(..), TTDecl, PReason(..), MetaInformation(..),                 Context, initContext, ctxtAlist, next_tvar,-                addToCtxt, setAccess, setInjective, setTotal, setMetaInformation, addCtxtDef, addTyDecl,+                addToCtxt, setAccess, setInjective, setTotal, setRigCount,+                setMetaInformation, addCtxtDef, addTyDecl,                 addDatatype, addCasedef, simplifyCasedef, addOperator,                 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,                 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,                 mapDefCtxt, tcReducible,                 lookupTotal, lookupTotalExact, lookupInjectiveExact,+                lookupRigCount, lookupRigCountExact,                 lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict,                 isCanonical, isDConName, canBeDConName, isTConName, isConName, isFnName,+                conGuarded,                 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,-                isUniverse) where+                isUniverse, linearCheck, linearCheckArg) where  import Idris.Core.CaseTree import Idris.Core.TT@@ -34,6 +37,7 @@ import Control.Monad.State import Data.Binary hiding (get, put) import qualified Data.Binary as B+import Data.List import Data.Maybe (listToMaybe) import Debug.Trace import GHC.Generics (Generic)@@ -72,6 +76,16 @@ --            | VLazy Env [Value] Term            | VTmp Int +canonical :: Value -> Bool+canonical (VP (DCon _ _ _) _ _) = True+canonical (VApp f a) = canonical f+canonical (VConstant _) = True+canonical (VType _) = True+canonical (VUType _) = True+canonical VErased = True+canonical _ = False++ instance Show Value where     show x = show $ evalState (quote 100 x) initEval @@ -132,7 +146,7 @@          (tm, limited st)  -- | Like normalise, but we only reduce functions that are marked as okay to--- inline, and lets +-- inline, and lets simplify :: Context -> Env -> TT Name -> TT Name simplify ctxt env t    = evalState (do val <- eval False ctxt [(sUN "lazy", 0),@@ -148,7 +162,7 @@                    quote 0 val) initEval  -- | Like simplify, but we only reduce functions that are marked as okay to--- inline, and don't reduce lets +-- inline, and don't reduce lets inlineSmall :: Context -> Env -> TT Name -> TT Name inlineSmall ctxt env t    = evalState (do val <- eval False ctxt []@@ -187,13 +201,13 @@  -- unbindEnv env (quote 0 (eval ctxt (bindEnv env t))) -finalEntry :: (Name, Binder (TT Name)) -> (Name, Binder (TT Name))-finalEntry (n, b) = (n, fmap finalise b)+finalEntry :: (Name, RigCount, Binder (TT Name)) -> (Name, RigCount, Binder (TT Name))+finalEntry (n, r, b) = (n, r, fmap finalise b)  bindEnv :: EnvTT n -> TT n -> TT n bindEnv [] tm = tm-bindEnv ((n, Let t v):bs) tm = Bind n (NLet t v) (bindEnv bs tm)-bindEnv ((n, b):bs)       tm = Bind n b (bindEnv bs tm)+bindEnv ((n, r, Let t v):bs) tm = Bind n (NLet t v) (bindEnv bs tm)+bindEnv ((n, r, b):bs)       tm = Bind n b (bindEnv bs tm)  unbindEnv :: EnvTT n -> TT n -> TT n unbindEnv [] tm = tm@@ -217,7 +231,7 @@   = case lookup n ns of          Just 0 -> return (False, ns)          Just i -> return $ (True, (n, abs (i-1)) : filter (\ (n', _) -> n/=n') ns)-         _ -> return $ if uf +         _ -> return $ if uf                           then (False, ns)                           else (True, (n, depthlimit) : filter (\ (n', _) -> n/=n') ns) @@ -254,6 +268,8 @@     atRepl = AtREPL `elem` opts     unfold = Unfold `elem` opts +    noFree = all canonical . map snd+     -- returns 'True' if the function should block     -- normal evaluation should return false     blockSimplify (CaseInfo inl always dict) n stk@@ -270,15 +286,15 @@                 | otherwise = cases_compiletime cd      ev ntimes stk top env (P _ n ty)-        | Just (Let t v) <- lookup n genv = ev ntimes stk top env v+        | Just (Let t v) <- lookupBinder n genv = ev ntimes stk top env v     ev ntimes_in stk top env (P Ref n ty)          = do let limit = if simpl then 100 else 10000               (u, ntimes) <- usable spec unfold limit n ntimes_in-              let red = u && (tcReducible n ctxt || spec || atRepl +              let red = u && (tcReducible n ctxt || spec || (atRepl && noFree env)                                 || runtime || unfold                                 || sUN "assert_total" `elem` stk)               if red then-               do let val = lookupDefAccExact n (spec || unfold || atRepl || runtime) ctxt+               do let val = lookupDefAccExact n (spec || unfold || (atRepl && noFree env) || runtime) ctxt                   case val of                     Just (Function _ tm, Public) ->                            ev ntimes (n:stk) True env tm@@ -325,7 +341,7 @@                 return $ VBind True n (Let t' v') (\x -> return sc')     ev ntimes stk top env (Bind n b sc)            = do b' <- vbind env b-                let n' = uniqueName n (map fst genv ++ map fst env)+                let n' = uniqueName n (map fstEnv genv ++ map fst env)                 return $ VBind True -- (vinstances 0 sc < 2)                                n' b' (\x -> ev ntimes stk False ((n', x):env) sc)        where vbind env t@@ -347,7 +363,7 @@                  evApply ntimes' stk top env [l',t',arg'] d'     -- Treat "assert_total" specially, as long as it's defined!     ev ntimes stk top env (App _ (App _ (P _ n@(UN at) _) _) arg)-       | Just (CaseOp _ _ _ _ _ _, _) <- lookupDefAccExact n (spec || atRepl || runtime) ctxt,+       | Just (CaseOp _ _ _ _ _ _, _) <- lookupDefAccExact n (spec || (atRepl && noFree env)|| runtime) ctxt,          at == txt "assert_total" && not (simpl || unfold)             = ev ntimes (n : stk) top env arg     ev ntimes stk top env (App _ f a)@@ -376,7 +392,7 @@           = apply ntimes stk top env f args      reapply ntimes stk top env f@(VP Ref n ty) args-       = let val = lookupDefAccExact n (spec || atRepl || runtime) ctxt in+       = let val = lookupDefAccExact n (spec || (atRepl && noFree env) || runtime) ctxt in          case val of               Just (CaseOp ci _ _ _ _ cd, acc) ->                  let (ns, tree) = getCases cd in@@ -391,18 +407,18 @@             = reapply ntimes stk top env f (a : args)     reapply ntimes stk top env v args = return v -    apply ntimes stk top env (VBind True n (Lam t) sc) (a:as)+    apply ntimes stk top env (VBind True n (Lam _ t) sc) (a:as)          = do a' <- sc a               app <- apply ntimes stk top env a' as               wknV 1 app     apply ntimes_in stk top env f@(VP Ref n ty) args          = do let limit = if simpl then 100 else 10000               (u, ntimes) <- usable spec unfold limit n ntimes_in-              let red = u && (tcReducible n ctxt || spec || atRepl +              let red = u && (tcReducible n ctxt || spec || (atRepl && noFree env)                                 || unfold || runtime                                 || sUN "assert_total" `elem` stk)               if red then-                 do let val = lookupDefAccExact n (spec || unfold || atRepl || runtime) ctxt+                 do let val = lookupDefAccExact n (spec || unfold || (atRepl && noFree env) || runtime) ctxt                     case val of                       Just (CaseOp ci _ _ _ _ cd, acc)                            | acc == Public || acc == Hidden ->@@ -508,7 +524,7 @@         | Just v <- findDefault alts      = return $ Just (amap, v)     chooseAlt env _ (VP _ n _, args) alts amap         | Just (ns, sc) <- findFn n alts  = return $ Just (updateAmap (zip ns args) amap, sc)-    chooseAlt env _ (VBind _ _ (Pi i s k) t, []) alts amap+    chooseAlt env _ (VBind _ _ (Pi _ i s k) t, []) alts amap         | Just (ns, sc) <- findFn (sUN "->") alts            = do t' <- t (VV 0) -- we know it's not in scope or it's not a pattern                 return $ Just (updateAmap (zip ns [s, t']) amap, sc)@@ -624,17 +640,17 @@         | x `elem` holes || y `elem` holes = return True         | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True         | otherwise = sameDefs ps x y-    ceq ps x (Bind n (Lam t) (App _ y (V 0)))+    ceq ps x (Bind n (Lam _ t) (App _ y (V 0)))           = ceq ps x (substV (P Bound n t) y)-    ceq ps (Bind n (Lam t) (App _ x (V 0))) y+    ceq ps (Bind n (Lam _ t) (App _ x (V 0))) y           = ceq ps (substV (P Bound n t) x) y-    ceq ps x (Bind n (Lam t) (App _ y (P Bound n' _)))+    ceq ps x (Bind n (Lam _ t) (App _ y (P Bound n' _)))         | n == n' = ceq ps x y-    ceq ps (Bind n (Lam t) (App _ x (P Bound n' _))) y+    ceq ps (Bind n (Lam _ t) (App _ x (P Bound n' _))) y         | n == n' = ceq ps x y -    ceq ps (Bind n (PVar t) sc) y = ceq ps sc y-    ceq ps x (Bind n (PVar t) sc) = ceq ps x sc+    ceq ps (Bind n (PVar _ t) sc) y = ceq ps sc y+    ceq ps x (Bind n (PVar _ t) sc) = ceq ps x sc     ceq ps (Bind n (PVTy t) sc) y = ceq ps sc y     ceq ps x (Bind n (PVTy t) sc) = ceq ps x sc @@ -650,7 +666,7 @@         where             ceqB ps (Let v t) (Let v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')             ceqB ps (Guess v t) (Guess v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')-            ceqB ps (Pi i v t) (Pi i' v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')+            ceqB ps (Pi r i v t) (Pi r' i' v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')             ceqB ps b b' = ceq ps (binderTy b) (binderTy b')     -- Special case for 'case' blocks - size of scope causes complications,     -- we only want to check the blocks themselves are valid and identical@@ -854,11 +870,14 @@  -- | Contexts used for global definitions and for proof state. They contain -- universe constraints and existing definitions.+-- Also store maximum RigCount of the name (can't bind a name at multiplicity+-- 1 in a RigW, for example) data Context = MkContext {                   next_tvar       :: Int,-                  definitions     :: Ctxt (Def, Injectivity, Accessibility, Totality, MetaInformation)+                  definitions     :: Ctxt TTDecl                 } deriving (Show, Generic) +type TTDecl = (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation)  -- | The initial empty context initContext = MkContext 0 emptyContext@@ -866,53 +885,59 @@  mapDefCtxt :: (Def -> Def) -> Context -> Context mapDefCtxt f (MkContext t !defs) = MkContext t (mapCtxt f' defs)-   where f' (!d, i, a, t, m) = f' (f d, i, a, t, m)+   where f' (!d, r, i, a, t, m) = f' (f d, r, i, a, t, m)  -- | Get the definitions from a context ctxtAlist :: Context -> [(Name, Def)]-ctxtAlist ctxt = map (\(n, (d, i, a, t, m)) -> (n, d)) $ toAlist (definitions ctxt)+ctxtAlist ctxt = map (\(n, (d, r, i, a, t, m)) -> (n, d)) $ toAlist (definitions ctxt)  veval ctxt env t = evalState (eval False ctxt [] env t []) initEval  addToCtxt :: Name -> Term -> Type -> Context -> Context addToCtxt n tm ty uctxt     = let ctxt = definitions uctxt-          !ctxt' = addDef n (Function ty tm, False, Public, Unchecked, EmptyMI) ctxt in+          !ctxt' = addDef n (Function ty tm, RigW, False, Public, Unchecked, EmptyMI) ctxt in           uctxt { definitions = ctxt' }  setAccess :: Name -> Accessibility -> Context -> Context setAccess n a uctxt     = let ctxt = definitions uctxt-          !ctxt' = updateDef n (\ (d, i, _, t, m) -> (d, i, a, t, m)) ctxt in+          !ctxt' = updateDef n (\ (d, r, i, _, t, m) -> (d, r, i, a, t, m)) ctxt in           uctxt { definitions = ctxt' }  setInjective :: Name -> Injectivity -> Context -> Context setInjective n i uctxt     = let ctxt = definitions uctxt-          !ctxt' = updateDef n (\ (d, _, a, t, m) -> (d, i, a, t, m)) ctxt in+          !ctxt' = updateDef n (\ (d, r, _, a, t, m) -> (d, r, i, a, t, m)) ctxt in           uctxt { definitions = ctxt' }  setTotal :: Name -> Totality -> Context -> Context setTotal n t uctxt     = let ctxt = definitions uctxt-          !ctxt' = updateDef n (\ (d, i, a, _, m) -> (d, i, a, t, m)) ctxt in+          !ctxt' = updateDef n (\ (d, r, i, a, _, m) -> (d, r, i, a, t, m)) ctxt in           uctxt { definitions = ctxt' } +setRigCount :: Name -> RigCount -> Context -> Context+setRigCount n rc uctxt+    = let ctxt = definitions uctxt+          !ctxt' = updateDef n (\ (d, _, i, a, t, m) -> (d, rc, i, a, t, m)) ctxt in+          uctxt { definitions = ctxt' }+ setMetaInformation :: Name -> MetaInformation -> Context -> Context setMetaInformation n m uctxt     = let ctxt = definitions uctxt-          !ctxt' = updateDef n (\ (d, i, a, t, _) -> (d, i, a, t, m)) ctxt in+          !ctxt' = updateDef n (\ (d, r, i, a, t, _) -> (d, r, i, a, t, m)) ctxt in           uctxt { definitions = ctxt' }  addCtxtDef :: Name -> Def -> Context -> Context addCtxtDef n d c = let ctxt = definitions c-                       !ctxt' = addDef n (d, False, Public, Unchecked, EmptyMI) $! ctxt in+                       !ctxt' = addDef n (d, RigW, False, Public, Unchecked, EmptyMI) $! ctxt in                        c { definitions = ctxt' }  addTyDecl :: Name -> NameType -> Type -> Context -> Context addTyDecl n nt ty uctxt     = let ctxt = definitions uctxt-          !ctxt' = addDef n (TyDecl nt ty, False, Public, Unchecked, EmptyMI) ctxt in+          !ctxt' = addDef n (TyDecl nt ty, RigW, False, Public, Unchecked, EmptyMI) ctxt in           uctxt { definitions = ctxt' }  addDatatype :: Datatype Name -> Context -> Context@@ -920,14 +945,14 @@     = let ctxt = definitions uctxt           ty' = normalise uctxt [] ty           !ctxt' = addCons 0 cons (addDef n-                     (TyDecl (TCon tag (arity ty')) ty, True, Public, Unchecked, EmptyMI) ctxt) in+                     (TyDecl (TCon tag (arity ty')) ty, RigW, True, Public, Unchecked, EmptyMI) ctxt) in           uctxt { definitions = ctxt' }   where     addCons tag [] ctxt = ctxt     addCons tag ((n, ty) : cons) ctxt         = let ty' = normalise uctxt [] ty in               addCons (tag+1) cons (addDef n-                  (TyDecl (DCon tag (arity ty') unique) ty, True, Public, Unchecked, EmptyMI) ctxt)+                  (TyDecl (DCon tag (arity ty') unique) ty, RigW, True, Public, Unchecked, EmptyMI) ctxt)  -- FIXME: Too many arguments! Refactor all these Bools. --@@ -961,33 +986,34 @@                                            (args_rt, sc_rt)                            op = (CaseOp (ci { case_inlinable = inlc })                                                 ty argtys ps_in ps_ct cdef,-                                 False, access, Unchecked, EmptyMI)+                                 RigW, False, access, Unchecked, EmptyMI)                        in return $ addDef n op ctxt --                    other -> tfail (Msg $ "Error adding case def: " ++ show other)          return uctxt { definitions = ctxt' } --- simplify a definition by inlining--- (Note: This used to be for totality checking, and now it's actually a--- no-op, but I'm keeping it here because I'll be putting it back with some--- more carefully controlled inlining at some stage. --- EB)-simplifyCasedef :: Name -> ErasureInfo -> Context -> TC Context-simplifyCasedef n ei uctxt+-- simplify a definition by unfolding interface methods+-- We need this for totality checking, because functions which use interfaces+-- in an implementation definition themselves need to have the implementation+-- inlined or it'll be treated as a higher order function that will potentially+-- loop.+simplifyCasedef :: Name -> [Name] -> [[Name]] -> ErasureInfo -> Context -> TC Context+simplifyCasedef n ufnames umethss ei uctxt    = do let ctxt = definitions uctxt         ctxt' <- case lookupCtxt n ctxt of-                   [(CaseOp ci ty atys [] ps _, inj, acc, tot, metainf)] ->+                   [(CaseOp ci ty atys [] ps _, rc, inj, acc, tot, metainf)] ->                       return ctxt -- nothing to simplify (or already done...)-                   [(CaseOp ci ty atys ps_in ps cd, inj, acc, tot, metainf)] ->+                   [(CaseOp ci ty atys ps_in ps cd, rc, inj, acc, tot, metainf)] ->                       do let ps_in' = map simpl ps_in                              pdef = map debind ps_in'                          CaseDef args sc _ <- simpleCase False (STerm Erased) False CompileTime emptyFC [] atys pdef ei                          return $ addDef n (CaseOp ci                                               ty atys ps_in' ps (cd { cases_compiletime = (args, sc) }),-                                              inj, acc, tot, metainf) ctxt+                                              rc, inj, acc, tot, metainf) ctxt                     _ -> return ctxt         return uctxt { definitions = ctxt' }   where-    depat acc (Bind n (PVar t) sc)+    depat acc (Bind n (PVar _ t) sc)         = depat (n : acc) (instantiate (P Bound n t) sc)     depat acc x = (acc, x)     debind (Right (x, y)) = let (vs, x') = depat [] x@@ -995,17 +1021,45 @@                                 (vs, x', y')     debind (Left x)       = let (vs, x') = depat [] x in                                 (vs, x', Impossible)-    simpl (Right (x, y)) = Right (x, y) -- inline uctxt [] y)+    simpl (Right (x, y))+         = if null ufnames then Right (x, y)+              else Right (x, unfold uctxt [] (map (\n -> (n, 1)) (uns y)) y)     simpl t = t +    -- Unfold the given name, interface methdods, and any function which uses it as+    -- an argument directly. This is specifically for finding applications of+    -- interface dictionaries and inlining them both for totality checking and for+    -- a small performance gain.+    uns tm = getNamesToUnfold ufnames umethss tm++    getNamesToUnfold :: [Name] -> [[Name]] -> Term -> [Name]+    getNamesToUnfold inames ms tm = nub $ inames ++ getNames Nothing tm ++ concat ms+      where+        getNames under fn@(App _ _ _)+            | (f, args) <- unApply fn+                 = let under' = case f of+                                     P _ fn _ -> Just fn+                                     _ -> Nothing+                                  in+                       getNames under f ++ concatMap (getNames under') args+        getNames (Just under) (P _ ref _)+            = if ref `elem` inames then [under] else []+        getNames under (Bind n (Let t v) sc)+            = getNames Nothing t +++              getNames Nothing v +++              getNames Nothing sc+        getNames under (Bind n b sc) = getNames Nothing (binderTy b) +++                                       getNames Nothing sc+        getNames _ _ = []+ addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) ->                Context -> Context addOperator n ty a op uctxt     = let ctxt = definitions uctxt-          ctxt' = addDef n (Operator ty a op, False, Public, Unchecked, EmptyMI) ctxt in+          ctxt' = addDef n (Operator ty a op, RigW, False, Public, Unchecked, EmptyMI) ctxt in           uctxt { definitions = ctxt' } -tfst (a, _, _, _, _) = a+tfst (a, _, _, _, _, _) = a  lookupNames :: Name -> Context -> [Name] lookupNames n ctxt@@ -1084,6 +1138,17 @@          Just (CaseOp ci _ _ _ _ _) -> tc_dictionary ci          _                          -> False +-- Is the name guarded by constructors in the term?+-- We assume the term is normalised, so no looking under 'let' for example.+conGuarded :: Context -> Name -> Term -> Bool+conGuarded ctxt n tm = guarded n tm+  where+    guarded n (P _ n' _) = n == n'+    guarded n ap@(App _ _ _)+        | (P _ f _, as) <- unApply ap,+          isConName f ctxt = any (guarded n) as+    guarded _ _ = False+ lookupP :: Name -> Context -> [Term] lookupP = lookupP_all False False @@ -1091,10 +1156,10 @@ lookupP_all all exact n ctxt    = do (n', def) <- names         p <- case def of-          (Function ty tm, inj, a, _, _)      -> return (P Ref n' ty, a)-          (TyDecl nt ty, _, a, _, _)        -> return (P nt n' ty, a)-          (CaseOp _ ty _ _ _ _, inj, a, _, _) -> return (P Ref n' ty, a)-          (Operator ty _ _, inj, a, _, _)     -> return (P Ref n' ty, a)+          (Function ty tm, _, inj, a, _, _)      -> return (P Ref n' ty, a)+          (TyDecl nt ty, _, _, a, _, _)        -> return (P nt n' ty, a)+          (CaseOp _ ty _ _ _ _, _, inj, a, _, _) -> return (P Ref n' ty, a)+          (Operator ty _ _, _, inj, a, _, _)     -> return (P Ref n' ty, a)         case snd p of           Hidden -> if all then return (fst p) else []           Private -> if all then return (fst p) else []@@ -1121,29 +1186,64 @@ lookupDefAcc n mkpublic ctxt     = map mkp $ lookupCtxt n (definitions ctxt)   -- io_bind a special case for REPL prettiness-  where mkp (d, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_pure"))-                                   then (d, Public) else (d, a)+  where mkp (d, _, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_pure"))+                                      then (d, Public) else (d, a)  lookupDefAccExact :: Name -> Bool -> Context ->                      Maybe (Def, Accessibility) lookupDefAccExact n mkpublic ctxt     = fmap mkp $ lookupCtxtExact n (definitions ctxt)   -- io_bind a special case for REPL prettiness-  where mkp (d, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_pure"))-                                   then (d, Public) else (d, a)+  where mkp (d, _, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_pure"))+                                      then (d, Public) else (d, a)  lookupTotal :: Name -> Context -> [Totality] lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)-  where mkt (d, inj, a, t, m) = t+  where mkt (d, _, inj, a, t, m) = t  lookupTotalExact :: Name -> Context -> Maybe Totality lookupTotalExact n ctxt = fmap mkt $ lookupCtxtExact n (definitions ctxt)-  where mkt (d, inj, a, t, m) = t+  where mkt (d, _, inj, a, t, m) = t +lookupRigCount :: Name -> Context -> [Totality]+lookupRigCount n ctxt = map mkt $ lookupCtxt n (definitions ctxt)+  where mkt (d, _, inj, a, t, m) = t++lookupRigCountExact :: Name -> Context -> Maybe RigCount+lookupRigCountExact n ctxt = fmap mkt $ lookupCtxtExact n (definitions ctxt)+  where mkt (d, rc, inj, a, t, m) = rc+ lookupInjectiveExact :: Name -> Context -> Maybe Injectivity lookupInjectiveExact n ctxt = fmap mkt $ lookupCtxtExact n (definitions ctxt)-  where mkt (d, inj, a, t, m) = inj+  where mkt (d, _, inj, a, t, m) = inj +-- Assume type is at least in whnfArgs form+linearCheck :: Context -> Type -> TC ()+linearCheck ctxt t = checkArgs t+  where+    checkArgs (Bind n (Pi RigW _ ty _) sc)+        = do linearCheckArg ctxt ty+             checkArgs (substV (P Bound n Erased) sc)+    checkArgs (Bind n (Pi _ _ _ _) sc)+          = checkArgs (substV (P Bound n Erased) sc)+    checkArgs _ = return ()++linearCheckArg :: Context -> Type -> TC ()+linearCheckArg ctxt ty = mapM_ checkNameOK (allTTNames ty)+  where+    checkNameOK f+       = case lookupRigCountExact f ctxt of+              Just Rig1 ->+                  tfail $ Msg $ show f ++ " can only appear in a linear binding"+              _ -> return ()++    checkArgs (Bind n (Pi RigW _ ty _) sc)+        = do mapM_ checkNameOK (allTTNames ty)+             checkArgs (substV (P Bound n Erased) sc)+    checkArgs (Bind n (Pi _ _ _ _) sc)+          = checkArgs (substV (P Bound n Erased) sc)+    checkArgs _ = return ()+ -- Check if a name is reducible in the type checker. Partial definitions -- are not reducible (so treated as a constant) tcReducible :: Name -> Context -> Bool@@ -1154,10 +1254,10 @@  lookupMetaInformation :: Name -> Context -> [MetaInformation] lookupMetaInformation n ctxt = map mkm $ lookupCtxt n (definitions ctxt)-  where mkm (d, inj, a, t, m) = m+  where mkm (d, _, inj, a, t, m) = m  lookupNameTotal :: Name -> Context -> [(Name, Totality)]-lookupNameTotal n = map (\(n, (_, _, _, t, _)) -> (n, t)) . lookupCtxtName n . definitions+lookupNameTotal n = map (\(n, (_, _, _, _, t, _)) -> (n, t)) . lookupCtxtName n . definitions   lookupVal :: Name -> Context -> [Value]@@ -1168,11 +1268,11 @@           (TyDecl nt ty) -> return (VP nt n (veval ctxt [] ty))           _ -> [] -lookupTyEnv :: Name -> Env -> Maybe (Int, Type)+lookupTyEnv :: Name -> Env -> Maybe (Int, RigCount, Type) lookupTyEnv n env = li n 0 env where   li n i []           = Nothing-  li n i ((x, b): xs)-             | n == x = Just (i, binderTy b)+  li n i ((x, r, b): xs)+             | n == x = Just (i, r, binderTy b)              | otherwise = li n (i+1) xs  -- | Create a unique name given context and other existing names