idris 1.3.1 → 1.3.2

raw patch · 121 files changed

+3469/−505 lines, 121 filesdep +parser-combinatorsdep ~aesondep ~code-pagedep ~containersbinary-addedPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: parser-combinators

Dependency ranges changed: aeson, code-page, containers, megaparsec, network, zip-archive

API changes (from Hackage documentation)

Files

• CHANGELOG.md +19/−0
• CONTRIBUTING.md +1/−1
• CONTRIBUTORS +1/−0
• INSTALL.md +20/−4
• appveyor.yml +4/−4
• docs/conf.py +2/−2
• docs/effects/impleff.rst +1/−1
• docs/effects/simpleeff.rst +2/−1
• docs/image/plusReducesProof.png binary
• docs/image/plusReducesProof.svg +339/−0
• 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/proofs/definitional.rst +231/−0
• docs/proofs/index.rst +3/−0
• docs/proofs/interactive.rst +224/−97
• docs/proofs/interactiveOld.rst +169/−0
• docs/proofs/propositional.rst +128/−0
• docs/reference/ffi.rst +42/−2
• docs/reference/index.rst +1/−0
• docs/reference/packages.rst +1/−1
• docs/reference/syntax-guide.rst +6/−0
• docs/reference/syntax-reference.rst +422/−0
• docs/st/examples.rst +1/−1
• docs/st/state.rst +1/−1
• docs/tutorial/conclusions.rst +1/−1
• docs/tutorial/interp.rst +1/−1
• docs/tutorial/packages.rst +1/−1
• docs/tutorial/views.rst +1/−2
• idris.cabal +9/−8
• jsrts/Runtime-javascript.js +5/−1
• jsrts/Runtime-node.js +12/−3
• libs/base/Control/Catchable.idr +1/−0
• libs/base/Control/Monad/Identity.idr +6/−0
• libs/base/Control/Monad/Writer.idr +3/−0
• libs/base/Data/IORef.idr +2/−0
• libs/base/Data/Vect.idr +280/−1
• libs/base/System.idr +13/−0
• libs/contrib/Control/Algebra/Lattice.idr +16/−0
• libs/contrib/Control/Algebra/Laws.idr +105/−0
• libs/contrib/Data/Bool/Extra.idr +52/−2
• libs/contrib/Data/Fin/Extra.idr +78/−1
• libs/contrib/Data/List/Extra.idr +14/−12
• libs/contrib/Data/Logic/Propositional.idr +161/−0
• libs/contrib/Data/Nat.idr +17/−0
• libs/contrib/Data/Nat/Fib.idr +50/−0
• libs/contrib/Data/Nat/Parity.idr +75/−0
• libs/contrib/Data/SortedMap.idr +4/−0
• libs/contrib/Interfaces/Proposition.idr +32/−0
• libs/contrib/Interfaces/Verified.idr +36/−0
• libs/contrib/Network/Cgi.idr +3/−0
• libs/contrib/Network/Socket/Data.idr +6/−6
• libs/contrib/Text/Lexer.idr +4/−4
• libs/contrib/contrib.ipkg +2/−0
• libs/prelude/Prelude/Bool.idr +1/−1
• libs/prelude/Prelude/File.idr +18/−6
• libs/prelude/Prelude/Interfaces.idr +8/−2
• libs/prelude/Prelude/List.idr +10/−4
• man/idris.1 +5/−1
• rts/idris_heap.c +2/−0
• rts/idris_rts.c +16/−17
• rts/idris_rts.h +3/−2
• rts/idris_stdfgn.c +26/−3
• rts/idris_stdfgn.h +2/−0
• rts/seL4/CMakeLists.txt +43/−0
• rts/seL4/Kbuild +0/−2
• rts/seL4/Kconfig +0/−9
• rts/seL4/Makefile +0/−33
• rts/seL4/README.md +5/−0
• rts/seL4/idris_main.c +2/−3
• rts/windows/win_utils.c +16/−0
• rts/windows/win_utils.h +9/−0
• src/IRTS/CodegenC.hs +2/−1
• src/IRTS/Compiler.hs +130/−13
• src/IRTS/JavaScript/AST.hs +1/−1
• src/IRTS/JavaScript/Codegen.hs +7/−4
• src/Idris/AbsSyntax.hs +2/−1
• src/Idris/AbsSyntaxTree.hs +1/−0
• src/Idris/CmdOptions.hs +11/−0
• src/Idris/Core/Evaluate.hs +7/−0
• src/Idris/Core/Execute.hs +13/−1
• src/Idris/Docs.hs +11/−6
• src/Idris/Elab/Clause.hs +5/−3
• src/Idris/IBC.hs +86/−6
• src/Idris/Options.hs +1/−1
• src/Idris/Output.hs +4/−3
• src/Idris/Package/Parser.hs +11/−7
• src/Idris/Parser.hs +179/−145
• src/Idris/Parser/Expr.hs +2/−2
• src/Idris/Parser/Helpers.hs +15/−9
• src/Idris/Parser/Ops.hs +1/−2
• src/Idris/Parser/Stack.hs +20/−9
• src/Idris/REPL/Parser.hs +5/−6
• stack-alt.yaml +25/−0
• stack.yaml +10/−5
• test/TestData.hs +5/−1
• test/TestRun.hs +20/−14
• test/docs001/expected +1/−1
• test/docs002/expected +3/−3
• test/docs003/expected +3/−1
• test/docs004/expected +3/−3
• test/docs005/expected +3/−1
• test/docs006/expected +1/−1
• test/error006/WithPatsNoWith.idr +11/−0
• test/error006/expected +14/−0
• test/ffi012/expected +1/−0
• test/ffi012/ffi012 +3/−0
• test/ffi012/ffi012.idr +14/−0
• test/ffi012/run +4/−0
• test/ffi013/expected +4/−0
• test/ffi013/ffi013.idr +5/−0
• test/ffi013/run +17/−0
• test/idrisdoc009/expected +2/−0
• test/interactive005/expected +3/−3
• test/interfaces001/expected +3/−2
• test/interfaces010/expected +0/−0
• test/interfaces010/interfaces010.idr +12/−0
• test/interfaces010/run +3/−0
• test/pkg008/expected +1/−3
• test/pkg008/maths.ipkg +1/−0
• test/pkg010/expected +6/−3

@@ -1,3 +1,22 @@+# New in 1.3.2++ Documentation added to proof section++## Library updates++ `openFile` opens the file in binary mode on Windows.++ Added library functions `clockTime` and `fRemove`++## Tool updates++ Modules no longer require building if imports have changed but all+  interfaces (i.e. types for names declared `export` and definitions of names+  declared `public export`) are unchanged.++ The result of calling `:doc` now details the accessbility of items as well as their totality.++## Miscellaneous updates++ Compiler flag `--optimise-nat-like-types` enables compilation+  of `Nat`-like type families to big integers. A type family+  is `Nat`-like if, after erasure, it has two constructors,+  one nullary, the other one with exactly one recursive field.+ # New in 1.3.1  ## Tool updates

@@ -83,7 +83,7 @@ 2. Clone your fork to your local machine:  ```-$ git clone git@github.com/<your github user name>/Idris-dev.git+$ git clone git@github.com:<your github user name>/Idris-dev.git ```  3. Add `idris-lang/Idris-dev` as a remote upstream

@@ -143,6 +143,7 @@ Mark Farrell Markus Klink Markus Pfeiffer+Martin Baker Mathnerd314 Mattias Lundell Matvey B. Aksenov

@@ -81,9 +81,9 @@ * `stack install`  Stack will install Idris (and related executables) into `$HOME/.local/bin/`-on Unix based systems and an appropriate place on Windows. The libraries that -are included with Idris (e.g. Builtins, Prelude) will 'install' into `<source -dir>/.stack_work/install/...` so you'll need to keep your source directory +on Unix based systems and an appropriate place on Windows. The libraries that+are included with Idris (e.g. Builtins, Prelude) will 'install' into `<source+dir>/.stack_work/install/...` so you'll need to keep your source directory around after you've installed Idris using Stack.  Of note: If you haven't used stack before commands will also setup the@@ -125,4 +125,20 @@  ``` PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig stack build-``` +```++## Issue with GHC on Ubuntu/Fedora++There is an upstream issue with GHC on some Ubuntu and Fedora machines.+The issue is that for GHC versions greater than 8.4.X linking to libFFI is broken.+See the following GHC issue page for more information:++  <https://gitlab.haskell.org/ghc/ghc/issues/15397>++This means that an Idris built with `libFFI` support will fail at runtime as the executable would not be able to find the correct `libffi` shared object.+This will cause the build to fail.+Specifically, one will see an error message along the lines of:++> error while loading shared libraries: libffi.so.7: cannot open shared object file: No such file or directory++We have supplied an alternative stack configuration file (`stack-alt.yaml`) that will use a version of GHC prior to the upstream issue being introduced.

@@ -5,15 +5,15 @@      mkdir C:\ghc -    Invoke-WebRequest "http://downloads.haskell.org/~ghc/8.2.1/ghc-8.2.1-x86_64-unknown-mingw32.tar.xz" -OutFile C:\ghc\ghc.tar.xz -UserAgent "Curl"+    Invoke-WebRequest "http://downloads.haskell.org/~ghc/8.4.3/ghc-8.4.3-x86_64-unknown-mingw32.tar.xz" -OutFile C:\ghc\ghc.tar.xz -UserAgent "Curl"      7z x C:\ghc\ghc.tar.xz -oC:\ghc      7z x C:\ghc\ghc.tar -oC:\ghc -    $env:PATH="$env:PATH;c:\ghc\ghc-8.2.1\bin;$HOME\AppData\Roaming\cabal\bin"+    $env:PATH="$env:PATH;c:\ghc\ghc-8.4.3\bin;$HOME\AppData\Roaming\cabal\bin" -    cabal update+    cabal v1-update      $env:current_posix=c:\msys64\usr\bin\cygpath -u $(pwd) @@ -22,6 +22,6 @@   MSYS2_PATH_TYPE: inherit build_script: - ps: >--    c:\msys64\usr\bin\bash -l -c "cd $env:current_posix && cabal install -fffi --enable-tests 2>&1"+    c:\msys64\usr\bin\bash -l -c "cd $env:current_posix && cabal v1-install -fffi --enable-tests 2>&1" test_script: - ps: c:\msys64\usr\bin\bash -l -c "cd $env:current_posix && make test_c 2>&1"

@@ -33,7 +33,7 @@ # ones. extensions = [     'sphinx.ext.todo',-    'sphinx.ext.pngmath', # imgmath is not supported on readthedocs.+#    'sphinx.ext.pngmath', # imgmath is not supported on readthedocs.     'sphinx.ext.ifconfig', ] @@ -61,7 +61,7 @@ # The short X.Y version. version = '1.3' # The full version, including alpha/beta/rc tags.-release = '1.3.1'+release = '1.3.2'  # The language for content autogenerated by Sphinx. Refer to documentation # for a list of supported languages.

@@ -144,7 +144,7 @@  **An implementation detail (aside):** The ``call`` function converts an ``Effect`` to a function in ``Eff``, given a proof that the effect-is available. This proof can be constructed automatically by , since+is available. This proof can be constructed automatically, since it is essentially an index into a statically known list of effects:  .. code-block:: idris

@@ -212,7 +212,8 @@  .. code-block:: idris -    data So : Bool -> Type = Oh : So True+    data So : Bool -> Type where+      Oh : So True      choose : (b : Bool) -> Either (So b) (So (not b)) 

binary file changed (absent → 14349 bytes)

@@ -0,0 +1,339 @@+<?xml version="1.0" encoding="UTF-8" standalone="no"?>+<!-- Created with Inkscape (http://www.inkscape.org/) -->++<svg+   xmlns:dc="http://purl.org/dc/elements/1.1/"+   xmlns:cc="http://creativecommons.org/ns#"+   xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"+   xmlns:svg="http://www.w3.org/2000/svg"+   xmlns="http://www.w3.org/2000/svg"+   xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"+   xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"+   width="210mm"+   height="297mm"+   viewBox="0 0 744.09448819 1052.3622047"+   id="svg2"+   version="1.1"+   inkscape:version="0.91 r13725"+   sodipodi:docname="plusReducesProof.svg">+  <defs+     id="defs4">+    <marker+       inkscape:stockid="Arrow1Mend"+       orient="auto"+       refY="0.0"+       refX="0.0"+       id="marker6540"+       style="overflow:visible;"+       inkscape:isstock="true">+      <path+         id="path6542"+         d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "+         style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"+         transform="scale(0.4) rotate(180) translate(10,0)" />+    </marker>+    <marker+       inkscape:stockid="Arrow1Mend"+       orient="auto"+       refY="0.0"+       refX="0.0"+       id="marker5748"+       style="overflow:visible;"+       inkscape:isstock="true">+      <path+         id="path5750"+         d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "+         style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"+         transform="scale(0.4) rotate(180) translate(10,0)" />+    </marker>+    <marker+       inkscape:isstock="true"+       style="overflow:visible;"+       id="marker5154"+       refX="0.0"+       refY="0.0"+       orient="auto"+       inkscape:stockid="Arrow1Mend"+       inkscape:collect="always">+      <path+         transform="scale(0.4) rotate(180) translate(10,0)"+         style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"+         d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "+         id="path5156" />+    </marker>+    <marker+       inkscape:stockid="Arrow1Mend"+       orient="auto"+       refY="0.0"+       refX="0.0"+       id="Arrow1Mend"+       style="overflow:visible;"+       inkscape:isstock="true"+       inkscape:collect="always">+      <path+         id="path4189"+         d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "+         style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"+         transform="scale(0.4) rotate(180) translate(10,0)" />+    </marker>+  </defs>+  <sodipodi:namedview+     id="base"+     pagecolor="#ffffff"+     bordercolor="#666666"+     borderopacity="1.0"+     inkscape:pageopacity="0.0"+     inkscape:pageshadow="2"+     inkscape:zoom="1"+     inkscape:cx="397.18872"+     inkscape:cy="520"+     inkscape:document-units="px"+     inkscape:current-layer="layer1"+     showgrid="false"+     inkscape:window-width="1110"+     inkscape:window-height="1011"+     inkscape:window-x="-4"+     inkscape:window-y="0"+     inkscape:window-maximized="0" />+  <metadata+     id="metadata7">+    <rdf:RDF>+      <cc:Work+         rdf:about="">+        <dc:format>image/svg+xml</dc:format>+        <dc:type+           rdf:resource="http://purl.org/dc/dcmitype/StillImage" />+        <dc:title></dc:title>+      </cc:Work>+    </rdf:RDF>+  </metadata>+  <g+     inkscape:label="Layer 1"+     inkscape:groupmode="layer"+     id="layer1">+    <text+       xml:space="preserve"+       style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"+       x="266"+       y="225.36221"+       id="text4136"+       sodipodi:linespacing="125%"><tspan+         sodipodi:role="line"+         id="tspan4138"+         x="266"+         y="225.36221">assumptions</tspan><tspan+         sodipodi:role="line"+         x="266"+         y="250.36221"+         id="tspan4140">(context)</tspan></text>+    <text+       sodipodi:linespacing="125%"+       id="text4142"+       y="238.36221"+       x="526"+       style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;"+       xml:space="preserve"><tspan+         id="tspan4146"+         y="238.36221"+         x="526"+         sodipodi:role="line">goal</tspan></text>+    <text+       xml:space="preserve"+       style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:12.5px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"+       x="420"+       y="289.36221"+       id="text4150"+       sodipodi:linespacing="125%"><tspan+         sodipodi:role="line"+         x="420"+         y="289.36221"+         id="tspan4152">(k : Nat) -&gt; (k = plus k 0) -&gt; S k = S (plus k 0)</tspan></text>+    <path+       style="fill:none;fill-rule:evenodd;stroke:#ff0000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;stroke-miterlimit:4;stroke-dasharray:none"+       d="m 241,262.3622 428,-1"+       id="path4154"+       inkscape:connector-curvature="0" />+    <path+       inkscape:connector-curvature="0"+       id="path4160"+       d="m 241,308.3622 428,-1"+       style="fill:none;fill-rule:evenodd;stroke:#ff0000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1" />+    <text+       sodipodi:linespacing="125%"+       id="text4162"+       y="312.36221"+       x="175"+       style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:12.5px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;"+       xml:space="preserve"><tspan+         id="tspan4164"+         y="312.36221"+         x="175"+         sodipodi:role="line">intro `{{k}}</tspan></text>+    <text+       sodipodi:linespacing="125%"+       id="text4166"+       y="333.36221"+       x="482"+       style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:12.5px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"+       xml:space="preserve"><tspan+         id="tspan4168"+         y="333.36221"+         x="482"+         sodipodi:role="line">(k = plus k 0) -&gt; S k = S (plus k 0)</tspan></text>+    <text+       xml:space="preserve"+       style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:12.5px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"+       x="324"+       y="334.36221"+       id="text4170"+       sodipodi:linespacing="125%"><tspan+         sodipodi:role="line"+         x="324"+         y="334.36221"+         id="tspan4172">k : Nat</tspan></text>+    <path+       style="fill:none;fill-rule:evenodd;stroke:#0000ff;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow1Mend)"+       d="m 441,294.3622 -73,30"+       id="path4174"+       inkscape:connector-curvature="0"+       sodipodi:nodetypes="cc" />+    <path+       style="fill:none;fill-rule:evenodd;stroke:#ff0000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"+       d="m 241,352.3622 428,-1"+       id="path5134"+       inkscape:connector-curvature="0" />+    <text+       xml:space="preserve"+       style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:12.5px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"+       x="171"+       y="355.36221"+       id="text5136"+       sodipodi:linespacing="125%"><tspan+         sodipodi:role="line"+         x="171"+         y="355.36221"+         id="tspan5138">intro `{{ih}}</tspan></text>+    <text+       xml:space="preserve"+       style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:12.5px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"+       x="570"+       y="372.36221"+       id="text5140"+       sodipodi:linespacing="125%"><tspan+         sodipodi:role="line"+         x="570"+         y="372.36221"+         id="tspan5142">S k = S (plus k 0)</tspan></text>+    <text+       sodipodi:linespacing="125%"+       id="text5144"+       y="378.36221"+       x="324"+       style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:12.5px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"+       xml:space="preserve"><tspan+         id="tspan5146"+         y="378.36221"+         x="324"+         sodipodi:role="line">k : Nat</tspan></text>+    <text+       sodipodi:linespacing="125%"+       id="text5150"+       y="393.36221"+       x="323"+       style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:12.5px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"+       xml:space="preserve"><tspan+         id="tspan5152"+         y="393.36221"+         x="323"+         sodipodi:role="line">ih : k = plus k 0</tspan></text>+    <path+       inkscape:connector-curvature="0"+       id="path5728"+       d="m 242,404.3622 428,-1"+       style="fill:none;fill-rule:evenodd;stroke:#ff0000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1" />+    <text+       sodipodi:linespacing="125%"+       id="text5730"+       y="408.36221"+       x="109"+       style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:12.5px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"+       xml:space="preserve"><tspan+         id="tspan5732"+         y="408.36221"+         x="109"+         sodipodi:role="line">rewriteWith (Var `{{ih}})</tspan></text>+    <text+       sodipodi:linespacing="125%"+       id="text5734"+       y="424.36221"+       x="587"+       style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:12.5px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"+       xml:space="preserve"><tspan+         id="tspan5736"+         y="424.36221"+         x="587"+         sodipodi:role="line">S k = S k </tspan></text>+    <text+       xml:space="preserve"+       style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:12.5px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"+       x="325"+       y="430.36221"+       id="text5738"+       sodipodi:linespacing="125%"><tspan+         sodipodi:role="line"+         x="325"+         y="430.36221"+         id="tspan5740">k : Nat</tspan></text>+    <path+       style="fill:none;fill-rule:evenodd;stroke:#0000ff;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker5748)"+       d="m 610,379.3622 1,29"+       id="path5742"+       inkscape:connector-curvature="0"+       sodipodi:nodetypes="cc" />+    <text+       xml:space="preserve"+       style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:12.5px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"+       x="324"+       y="445.36221"+       id="text5744"+       sodipodi:linespacing="125%"><tspan+         sodipodi:role="line"+         x="324"+         y="445.36221"+         id="tspan5746">ih : k = plus k 0</tspan></text>+    <path+       inkscape:connector-curvature="0"+       id="path7294"+       d="m 418,460.3622 -2,-199"+       style="fill:none;fill-rule:evenodd;stroke:#ff0000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"+       sodipodi:nodetypes="cc" />+    <path+       sodipodi:nodetypes="cc"+       inkscape:connector-curvature="0"+       id="path5148"+       d="m 519,339.3622 -107,44"+       style="fill:none;fill-rule:evenodd;stroke:#0000ff;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker5154)" />+    <path+       style="fill:none;fill-rule:evenodd;stroke:#0000ff;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:12, 2;stroke-dashoffset:0;stroke-opacity:1"+       d="m 609,391.3622 -197,49"+       id="path6538"+       inkscape:connector-curvature="0"+       sodipodi:nodetypes="cc" />+    <path+       style="fill:none;fill-rule:evenodd;stroke:#ff0000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"+       d="m 242,458.3622 428,-1"+       id="path7308"+       inkscape:connector-curvature="0" />+    <text+       xml:space="preserve"+       style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:12.5px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"+       x="177"+       y="462.36221"+       id="text7310"+       sodipodi:linespacing="125%"><tspan+         sodipodi:role="line"+         x="177"+         y="462.36221"+         id="tspan7312">reflexivity</tspan></text>+  </g>+</svg>

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

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

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

@@ -0,0 +1,231 @@+In order to understand how to write proofs in Idris I think its worth clarifying some fundamentals, such as,++-  Propositions and judgments+-  Boolean and constructive logic+-  Curry-Howard correspondence+-  Definitional and propositional equalities+-  Axiomatic and constructive approaches++Propositions and Judgments+==========================++Propositions are the subject of our proofs, before the proof then we can't formally say if they are true or not. If the proof is successful then the result is a 'judgment'.+For instance, if the ``proposition`` is,+++-------++| 1+1=2 |++-------+++When we prove it, the ``judgment`` is,+++------------++| 1+1=2 true |++------------+++Or if the ``proposition`` is,+++-------++| 1+1=3 |++-------+++Obviously  we can't prove it is true, but it is still a valid proposition and perhaps we can prove it is false so the ``judgment`` is, +++-------------++| 1+1=3 false |++-------------+++This may seem a bit pedantic but it is important to be careful,  in mathematics not every proposition is true or false for instance, a proposition may be unproven or even unprovable.++So the logic here is different from the logic that comes from boolean algebra. In that case what is not true is false and what is not false is true. The logic we are using here does not have this 'law of excluded middle' so we have to be careful not to use it.++A false proposition is taken to be a contradiction and if we have a contradiction then we can prove anything, so we need to avoid this. Some languages, used in proof assistants, prevent contradictions but such languages cannot be Turing complete, so Idris does not prevent contradictions.++The logic we are using  is called constructive (or sometimes intuitional) because we are constructing a 'database' of judgments.++There are also many other types of logic, another important type of logic for Idris programmers is '``linear logic``' but that's not discussed on this page.++Curry-Howard correspondence+===========================++So how to we relate these proofs to Idris programs? It turns out that there is a correspondence between constructive logic and type theory. They are the same structure and we can switch backward and forward between the two notations because they are the same thing.++The way that this works is that a  proposition is a type so this,++.. code-block:: idris++   Idris> 1+1=2+   2 = 2 : Type++is a proposition and it is also a type. This is built into Idris so when an '=' equals sign appears in a function type an equality type is generated. The following will also produce an equality type:+++.. code-block:: idris++   Idris> 1+1=3+   2 = 3 : Type++Both of these are valid propositions so both are valid equality types. But how do we represent true judgment, that is, how do we denote 1+1=2 is true but not 1+1=3.+A type that is true is inhabited, that is, it can be constructed. An equality type has only one constructor 'Refl' so a proof of 1+1=2 is++.. code-block:: idris++   onePlusOne : 1+1=2+   onePlusOne = Refl++So how can Refl, which is a constructor without any parameters, construct an equality type? If we type it on its own then it can't:++.. code-block:: idris++  Idris> Refl+  (input):Can't infer argument A to Refl, Can't infer argument x to Refl++So it must pattern match on its return type:++.. code-block:: idris++    Idris> the (1=1) Refl+    Refl : 1 = 1++So now that we can represent propositions as types other aspects of propositional logic can also be translated to types as follows:+++----------+-------------------+--------------------------++|          | propositions      | example of possible type |++----------+-------------------+--------------------------++| A        | x=y               |                          |++----------+-------------------+--------------------------++| B        | y=z               |                          |++----------+-------------------+--------------------------++| and      | A /\ B            | Pair(x=y,y=z)            |++----------+-------------------+--------------------------++| or       | A \/ B            | Either(x=y,y=z)          |++----------+-------------------+--------------------------++| implies  | A -> B            | (x=y) -> (y=x)           |++----------+-------------------+--------------------------++| for all  | y=z               |                          |++----------+-------------------+--------------------------++| exists   | y=z               |                          |++----------+-------------------+--------------------------++++And (conjunction)+-----------------++We can have a type which corresponds to conjunction:++.. code-block:: idris++   AndIntro : a -> b -> A a b++There is a built in type called 'Pair'.++Or (disjunction)+----------------++We can have a type which corresponds to disjunction:++.. code-block:: idris++   data Or : Type -> Type -> Type where+   OrIntroLeft : a -> A a b+   OrIntroRight : b -> A a b++There is a built in type called 'Either'.++Definitional and Propositional Equalities+=========================================++We have seen that  we can 'prove' a type by finding a way to construct a term. In the case of equality types there is only one constructor which is 'Refl'.+We have also seen that each side of the equation does not have to be identical like '2=2'. It is enough that both sides are ``definitionaly equal`` like this:++.. code-block:: idris++   onePlusOne : 1+1=2+   onePlusOne = Refl++So both sides of this equation nomalise to 2 and so Refl will type match and the proposition is proved.++We don't have to stick to terms, can also use symbolic parameters so the following  will compile:++.. code-block:: idris++   varIdentity : m = m+   varIdentity = Refl++If a proposition/equality type is not definitionaly equal but is still true then it is ``propositionaly equal``. In this case we may still be able to prove it but some steps in the proof may require us to add something into the terms or at least to take some sideways steps to get to a proof.++Especially when working with equalities containing variable terms (inside functions) it can be hard to know which equality types are definitially equal, in this example plusReducesL is '``definitially equal``' but plusReducesR is not (although it is '``propositionaly equal``'). The only difference between them is the order of the operands.++.. code-block:: idris++   plusReducesL : (n:Nat) -> plus Z n = n+   plusReducesL n = Refl++   plusReducesR : (n:Nat) -> plus n Z = n+   plusReducesR n = Refl++plusReducesR gives the following error:+++.. code-block:: idris++   - + Errors (1)+   `-- proof.idr line 6 col 17:+     When checking right hand side of plusReducesR with expected type+             plus n 0 = n++     Type mismatch between+             n = n (Type of Refl)+     and+             plus n 0 = n (Expected type)++     Specifically:+             Type mismatch between+                     n+             and+                     plus n 0++So why is 'Refl' able to prove some equality types but not others?++The first answer is that 'plus' is defined in such a way that it splits on its first argument so it is simple to prove when 0 is the first argument but not the second. So what is the general way to know if Refl will work?++If an equality type can be proved/constructed by using Refl alone it is known as a ``definitional equality``. In order to be definitinally equal both sides of the equation must normalise to unique values. That is, each step in the proof must reduce the term so each step is effectively forced.++So when we type 1+1 in Idris it is immediately converted to 2 because definitional equality is built in.++.. code-block:: idris++    Idris> 1+1+    2 : Integer++In the following pages we discuss how to resolve propositionaly equalies.++Axiomatic and Constructive Approaches+=====================================++How should we define types so that  we can do proofs on them? In the natural numbers with plus example we could have started by treating it as a group based on the plus operator. So we have axioms:++-  for all x,y : ``x+y=y+x``+-  for all x: ``x + 0 = x = 0 + x``+-  for all x,y,z: ``(x + y) + z = x + (x + z)``++Then we can implement '+' so that it respects these axioms (presumably implemented in hardware).++These are axioms, that is a propositions/types that are asserted to be true without proof. In Idris we can use the 'postulate' keyword +++.. code-block:: idris++   commutePlus ``postulate``: x -> y -> plus x y = plus y x++Alternatively we could define the natural numbers based on Zero and Successor. The axioms above then become derived rules and we also gain the ability to do inductive proofs.++As we know, Idris uses both of these approaches with automatic coercion between them which gives the best of both worlds.++So what can we learn from this to implement out own types:++-  Should we try to implement both approaches?+-  Should we define our types by constructing up from primitive types?++Proof theory affects these design decisions.++

@@ -18,8 +18,11 @@ .. toctree::    :maxdepth: 1 +   definitional    pluscomm    inductive    patterns+   propositional    interactive+   interactiveOld 

@@ -1,16 +1,103 @@-***************************************-DEPRECATED: Interactive Theorem Proving-***************************************+***************************+Interactive Theorem Proving+*************************** -.. warning::-   The interactive theorem-proving interface documented here has been-   deprecated in favor of :ref:`elaborator-reflection`.+Idris supports interactive theorem proving via elaborator reflection. -Idris also supports interactive theorem proving via tactics. This-is generally not recommended to be used directly, but rather used as a-mechanism for building proof automation which is beyond the scope of this-tutorial. In this section, we briefly discus tactics.+:ref:`elaborator-reflection` is also used to convert high-level Idris code into+the core language and for customising the language. Here we show how to use it+to interactively construct proofs. +The primary purpose of the elaboration mechanism is to elaborate Idris and so it+is not optimised to work as a proof assistant, however it can interactively+construct proofs as described on this page.++Elab and Pruviloj Libraries+===========================++Elaborator reflection is defined in prelude/Language/Reflection/Elab.idr+and pruviloj is defined in Idris-dev/libs/pruviloj/++``Elab`` defines the basics such as: solve, attack, intro, compute,+rewriteWith and others.+``pruviloj`` defines some more advanced derived commands such as:+reflexivity and others.++To use ``pruviloj`` call Idris with the "-p pruviloj" option and add:++.. code-block:: idris++    import Pruviloj+    import Pruviloj.Induction++to the top of your file.++It is useful to get the docs at the REPL by using the ``:doc`` command, and+search the docstrings using ``:apropos``. So to introduce the functions from+Elab and Pruviloj, that we will need for the following example, here are+their docstrings:++.. code-block:: idris++    *plusReducesZ> :doc solve+    Language.Reflection.Elab.Tactics.solve : Elab ()+        Substitute a guess into a hole.++.. code-block:: idris++    *plusReducesZ> :doc attack+    Language.Reflection.Elab.Tactics.attack : Elab ()+        Convert a hole to make it suitable for bindings - that is, transform+        it such that it has the form ?h : t . h as opposed to ?h : t . f h.++        The binding tactics require that a hole be directly under its binding,+        or else the scopes of the generated terms won't make sense. This+        tactic creates a new hole of the proper form, and points the old hole+        at it.++.. code-block:: idris++    *plusReducesZ> :doc intro+    Language.Reflection.Elab.Tactics.intro : (n : TTName) -> Elab ()+        Introduce a lambda binding around the current hole and focus on the+        body. Requires that the hole be in binding form (use attack).+        Arguments:+            n : TTName  -- the name to use for the argument++.. code-block:: idris++    *plusReducesZ> :doc compute+    Language.Reflection.Elab.Tactics.compute : Elab ()+        Normalise the goal.++.. code-block:: idris++    *plusReducesZ> :doc rewriteWith+    Language.Reflection.Elab.Tactics.rewriteWith : Raw -> Elab ()+        Attempt to rewrite the goal using an equality.++        The tactic searches the goal for applicable subterms, and constructs a+        context for replace using them. In some cases, this is not possible,+        and replace must be called manually with an appropriate context.++        Because this tactic internally introduces a let binding, it requires+        that the hole be immediately under its binder (use attack if it might+        not be).++Here is the command from pruviloj that we will need for the example on+this page:++.. code-block:: idris++    *plusReducesZ> :doc reflexivity+    Pruviloj.Core.reflexivity : Elab ()+        A special-purpose tactic that attempts to solve a goal using Refl.+        This is useful for ensuring that goals in fact are trivial when+        developing or testing other tactics; otherwise, consider using search.++Interactive Example: plusReduces+================================+ One way to write proofs interactively is to write the general *structure* of the proof, and use the interactive mode to complete the details. Consider the following definition, proved in :ref:`sect-theorems`:@@ -25,145 +112,185 @@  .. code-block:: idris +    import Pruviloj+    import Pruviloj.Induction+     plusReducesZ' : (n:Nat) -> n = plus n Z     plusReducesZ' Z     = ?plusredZ_Z     plusReducesZ' (S k) = let ih = plusReducesZ' k in                           ?plusredZ_S  On running , two global names are created, ``plusredZ_Z`` and-``plusredZ_S``, with no definition. We can use the ``:m`` command at the-prompt to find out which holes are still to be solved (or, more-precisely, which functions exist but have no definitions), then the-``:t`` command to see their types:+``plusredZ_S``, with no definition.  .. code-block:: idris -    *theorems> :m-    Global holes:-            [plusredZ_S,plusredZ_Z]+    *theorems> : idris plusReducesZ.idr -p pruviloj -.. code-block:: idris+    .  /  _/___/ /____(_)____+       / // __  / ___/ / ___/     Version 1.2.0+     _/ // /_/ / /  / (__  )      http://www.idris-lang.org/+    /___/\__,_/_/  /_/____/       Type :? for help -    *theorems> :t plusredZ_Z-    plusredZ_Z : Z = plus Z Z+    Idris is free software with ABSOLUTELY NO WARRANTY.+    For details type :warranty.+    Holes: Main.plusredZ_S, Main.plusredZ_Z -    *theorems> :t plusredZ_S-    plusredZ_S : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z+This tells us that we have two holes Main.plusredZ_S and Main.plusredZ_Z. We can solve+these separately, ``plusredZ_Z`` is the simplest so we will do that first. -The ``:p`` command enters interactive proof mode, which can be used to-complete the missing definitions.+The ``:elab plusredZ_Z`` command enters interactive elaboration mode, which can be used to+complete the missing definition for plusredZ_Z.  .. code-block:: idris -    *theorems> :p plusredZ_Z+    *plusReducesZ> :elab plusredZ_Z -    ---------------------------------- (plusredZ_Z) ---------    {hole0} : Z = plus Z Z+    ----------                 Goal:                  ----------+    {hole_0} : 0 = 0 -This gives us a list of premises (above the line; there are none here)-and the current goal (below the line; named ``{hole0}`` here). At the-prompt we can enter tactics to direct the construction of the proof. In-this case, we can normalise the goal with the ``compute`` tactic:+This has been normalised to ``0 = 0`` so now we have to prove that ``0`` equals ``0``, which+is easy to prove by reflexivity from the pruviloj library:  .. code-block:: idris -    -plusredZ_Z> compute--    ---------------------------------- (plusredZ_Z) ---------    {hole0} : Z = Z+    -Main.plusredZ_Z> reflexivity+    plusredZ_Z: No more goals. -Now we have to prove that ``Z`` equals ``Z``, which is easy to prove by-``Refl``. To apply a function, such as ``Refl``, we use ``refine`` which-introduces subgoals for each of the function’s explicit arguments-(``Refl`` has none):+This tells us that the proof is complete. We can now leave the interactive mode which+we entered with the ``:elab`` command. We do this with the ``:qed`` command:  .. code-block:: idris -    -plusredZ_Z> refine Refl-    plusredZ_Z: no more goals--Here, we could also have used the ``trivial`` tactic, which tries to-refine by ``Refl``, and if that fails, tries to refine by each name in-the local context. When a proof is complete, we use the ``qed`` tactic-to add the proof to the global context, and remove the hole from the-unsolved holes list. This also outputs a trace of the proof:--.. code-block:: idris+    -Main.plusredZ_Z> :qed+    Proof completed!+    Main.plusredZ_Z = %runElab (do reflexivity)+    Holes: Main.plusredZ_S -    -plusredZ_Z> qed-    plusredZ_Z = proof-        compute-        refine Refl+This gives us a trace of the proof which is ``plusredZ_Z = %runElab (do reflexivity)``. We+can cut & paste this into the hole in the original file. This also tells us that we+have another hole ``Main.plusredZ_S`` remaining. -.. code-block:: idris+This remaining proof is bit more complicated, the following diagram gives an overview: -    *theorems> :m-    Global holes:-            [plusredZ_S]+|image| -The ``:addproof`` command, at the interactive prompt, will add the proof-to the source file (effectively in an appendix). Let us now prove the-other required lemma, ``plusredZ_S``:+We approach this remaining proof in the same way by using the ``:elab`` command:  .. code-block:: idris -    *theorems> :p plusredZ_S+    *plusReducesZ> :elab plusredZ_S -    ---------------------------------- (plusredZ_S) ---------    {hole0} : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z +    ----------                 Goal:                  ----------+    {hole_0} : (k : Nat) -> (k = plus k 0) -> S k = S (plus k 0)+ In this case, the goal is a function type, using ``k`` (the argument accessible by pattern matching) and ``ih`` — the local variable containing the result of the recursive call. We can introduce these as-premises using the ``intro`` tactic twice (or ``intros``, which-introduces all arguments as premises). This gives:+assumptions using the ``intro`` tactic twice. The parameter is entered as+a constant of type ``TTName`` which is entered as a backtick with double+braces `{{ih}}. This gives:  .. code-block:: idris -      k : Nat-      ih : k = plus k Z-    ---------------------------------- (plusredZ_S) ---------    {hole2} : S k = plus (S k) Z+    -Main.plusredZ_S> intro `{{k}} -Since plus is defined by recursion on its first argument, the term-``plus (S k) Z`` in the goal can be simplified, so we use ``compute``.+    ----------              Assumptions:              ----------+     k : Nat+    ----------                 Goal:                  ----------+    {hole_0} : (k = plus k 0) -> S k = S (plus k 0)+    -Main.plusredZ_S> intro `{{ih}} +    ----------              Assumptions:              ----------+     k : Nat+     ih : k = plus k 0+    ----------                 Goal:                  ----------+    {hole_0} : S k = S (plus k 0)++We know, from the type of ``ih``, that ``k = plus k 0``, so we would+like to use this knowledge to replace ``plus k 0`` in the goal with+``k``. We can achieve this with the ``rewriteWith`` tactic:+ .. code-block:: idris -      k : Nat-      ih : k = plus k Z-    ---------------------------------- (plusredZ_S) ---------    {hole2} : S k = S (plus k Z)+    -Main.plusredZ_S> rewriteWith (Var `{{ih}}) -We know, from the type of ``ih``, that ``k = plus k Z``, so we would-like to use this knowledge to replace ``plus k Z`` in the goal with-``k``. We can achieve this with the ``rewrite`` tactic:+    ----------              Assumptions:              ----------+     k : Nat+     ih : k = plus k 0+    ----------                 Goal:                  ----------+    {hole_0} : S k = S k +The ``rewriteWith`` tactic takes an equality proof as an argument, and tries+to rewrite the goal using that proof. The ih value is entered as a constant+of type ``TTName`` which is entered as a backtick with double braces `{{ih}} but+``rewriteWith`` requires an expression of type ``Raw``, rather than just a name,+so the Var constructor is used to make a variable. Here, it results in an equality+which is trivially provable using reflexivity:+ .. code-block:: idris -    -plusredZ_S> rewrite ih+    -Main.plusredZ_S> reflexivity+    plusredZ_S: No more goals.+    -Main.plusredZ_S> :qed+    Proof completed!+    Main.plusredZ_S = %runElab (do intro `{{k}}+                                   intro `{{ih}}+                                   rewriteWith (Var `{{ih}})+                                   reflexivity) -      k : Nat-      ih : k = plus k Z-    ---------------------------------- (plusredZ_S) ---------    {hole3} : S k = S k+We can't just cut & paste this into the hole in the original file like this: -    -plusredZ_S>+.. code-block:: idris -The ``rewrite`` tactic takes an equality proof as an argument, and tries-to rewrite the goal using that proof. Here, it results in an equality-which is trivially provable:+  import Pruviloj+  import Pruviloj.Induction +  %language ElabReflection++  plusReducesZ' : (n:Nat) -> n = plus n Z+  plusReducesZ' Z     = %runElab (do reflexivity)+  plusReducesZ' (S k) = let ih = plusReducesZ' k in+                      (%runElab (do intro `{{k}}+                               intro `{{ih}}+                               rewriteWith (Var `{{ih}})+                               reflexivity)+                      )++because this gives the following error:+ .. code-block:: idris -    -plusredZ_S> trivial-    plusredZ_S: no more goals-    -plusredZ_S> qed-    plusredZ_S = proof {-        intros;-        rewrite ih;-        trivial;-    }+  Idris> :load elabInteractiveEx2.idr+  elabInteractiveEx2.idr:10:32:+     |+  10 |                                intro `{{ih}}+     |                                ^+  unexpected "in"+  expecting dependent type signature -Again, we can add this proof to the end of our source file using the-``:addproof`` command at the interactive prompt.+However if we put the proof into a separate function like this:++.. code-block:: idris++  import Pruviloj+  import Pruviloj.Induction++  %language ElabReflection++  plusredZ_S : (k : Nat) -> (ih:(k = plus k Z)) -> (S k = S (plus k Z))+  plusredZ_S = %runElab (do intro `{{k}}+                            intro `{{ih}}+                            rewriteWith (Var `{{ih}})+                            reflexivity)++  plusReducesZ' : (n:Nat) -> n = plus n Z+  plusReducesZ' Z     = %runElab (do reflexivity)+  plusReducesZ' (S k) = let ih = plusReducesZ' k in plusredZ_S k ih++This then loads.++.. [#f1] https://github.com/idris-lang/Idris-dev/issues/4556++.. |image| image:: ../image/plusReducesProof.png

@@ -0,0 +1,169 @@+**************************************************************+DEPRECATED: Interactive Theorem Proving Using Old Tactics Code+**************************************************************++.. warning::+   The interactive theorem-proving interface documented here has been+   deprecated in favor of :ref:`elaborator-reflection`.++Idris also supports interactive theorem proving via tactics. This+is generally not recommended to be used directly, but rather used as a+mechanism for building proof automation which is beyond the scope of this+tutorial. In this section, we briefly discus tactics.++One way to write proofs interactively is to write the general *structure* of+the proof, and use the interactive mode to complete the details.+Consider the following definition, proved in :ref:`sect-theorems`:++.. code-block:: idris++    plusReduces : (n:Nat) -> plus Z n = n++We’ll be constructing the proof by *induction*, so we write the cases for ``Z``+and ``S``, with a recursive call in the ``S`` case giving the inductive+hypothesis, and insert *holes* for the rest of the definition:++.. code-block:: idris++    plusReducesZ' : (n:Nat) -> n = plus n Z+    plusReducesZ' Z     = ?plusredZ_Z+    plusReducesZ' (S k) = let ih = plusReducesZ' k in+                          ?plusredZ_S++On running , two global names are created, ``plusredZ_Z`` and+``plusredZ_S``, with no definition. We can use the ``:m`` command at the+prompt to find out which holes are still to be solved (or, more+precisely, which functions exist but have no definitions), then the+``:t`` command to see their types:++.. code-block:: idris++    *theorems> :m+    Global holes:+            [plusredZ_S,plusredZ_Z]++.. code-block:: idris++    *theorems> :t plusredZ_Z+    plusredZ_Z : Z = plus Z Z++    *theorems> :t plusredZ_S+    plusredZ_S : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z++The ``:p`` command enters interactive proof mode, which can be used to+complete the missing definitions.++.. code-block:: idris++    *theorems> :p plusredZ_Z++    ---------------------------------- (plusredZ_Z) --------+    {hole0} : Z = plus Z Z++This gives us a list of premises (above the line; there are none here)+and the current goal (below the line; named ``{hole0}`` here). At the+prompt we can enter tactics to direct the construction of the proof. In+this case, we can normalise the goal with the ``compute`` tactic:++.. code-block:: idris++    -plusredZ_Z> compute++    ---------------------------------- (plusredZ_Z) --------+    {hole0} : Z = Z++Now we have to prove that ``Z`` equals ``Z``, which is easy to prove by+``Refl``. To apply a function, such as ``Refl``, we use ``refine`` which+introduces subgoals for each of the function’s explicit arguments+(``Refl`` has none):++.. code-block:: idris++    -plusredZ_Z> refine Refl+    plusredZ_Z: no more goals++Here, we could also have used the ``trivial`` tactic, which tries to+refine by ``Refl``, and if that fails, tries to refine by each name in+the local context. When a proof is complete, we use the ``qed`` tactic+to add the proof to the global context, and remove the hole from the+unsolved holes list. This also outputs a trace of the proof:++.. code-block:: idris++    -plusredZ_Z> qed+    plusredZ_Z = proof+        compute+        refine Refl++.. code-block:: idris++    *theorems> :m+    Global holes:+            [plusredZ_S]++The ``:addproof`` command, at the interactive prompt, will add the proof+to the source file (effectively in an appendix). Let us now prove the+other required lemma, ``plusredZ_S``:++.. code-block:: idris++    *theorems> :p plusredZ_S++    ---------------------------------- (plusredZ_S) --------+    {hole0} : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z++In this case, the goal is a function type, using ``k`` (the argument+accessible by pattern matching) and ``ih`` — the local variable+containing the result of the recursive call. We can introduce these as+premises using the ``intro`` tactic twice (or ``intros``, which+introduces all arguments as premises). This gives:++.. code-block:: idris++      k : Nat+      ih : k = plus k Z+    ---------------------------------- (plusredZ_S) --------+    {hole2} : S k = plus (S k) Z++Since plus is defined by recursion on its first argument, the term+``plus (S k) Z`` in the goal can be simplified, so we use ``compute``.++.. code-block:: idris++      k : Nat+      ih : k = plus k Z+    ---------------------------------- (plusredZ_S) --------+    {hole2} : S k = S (plus k Z)++We know, from the type of ``ih``, that ``k = plus k Z``, so we would+like to use this knowledge to replace ``plus k Z`` in the goal with+``k``. We can achieve this with the ``rewrite`` tactic:++.. code-block:: idris++    -plusredZ_S> rewrite ih++      k : Nat+      ih : k = plus k Z+    ---------------------------------- (plusredZ_S) --------+    {hole3} : S k = S k++    -plusredZ_S>++The ``rewrite`` tactic takes an equality proof as an argument, and tries+to rewrite the goal using that proof. Here, it results in an equality+which is trivially provable:++.. code-block:: idris++    -plusredZ_S> trivial+    plusredZ_S: no more goals+    -plusredZ_S> qed+    plusredZ_S = proof {+        intros;+        rewrite ih;+        trivial;+    }++Again, we can add this proof to the end of our source file using the+``:addproof`` command at the interactive prompt.

@@ -0,0 +1,128 @@+This page attempts to explain some of the techniques used in Idris to prove propositional equalities.++Proving Propositional Equality+==============================++We have seen that definitional equalities can be proved using Refl since they always normalise to unique values that can be compared directly.++However with propositional equalities we are using symbolic variables they do not always normalse.++So to take the previous example:++plusReducesR : (n:Nat) -> plus n Z = n++In this case 'plus n Z' does not normalise to n. Even though both sides are equal we cannot pattern match Refl.++If the pattern match cannot match for all 'n' then the way around this is to separately match all possible values of 'n'. In the case of natural numbers we do this by induction.++So here:++.. code-block:: idris++   plusReducesR : n = plus n 0+   plusReducesR {n = Z} = Refl+   plusReducesR {n = (S k)} = let rec = plus_commutes_Z {n=k} in+                                  rewrite rec in Refl++we don't call Refl to match on 'n = plus n 0' forall 'n' we call it for every number separately. So, in the second line, the pattern matcher knows to substitute Z for n in the type being matched. This uses 'rewrite' which is explained below.++Replace+=======++This implements the 'indiscernability of identicals' principle, if two terms are equal then they have the same properties. In other words, if x=y, then we can substitute y for x in any expression. In our proofs we can express this as:++   if x=y+   then P x = P y++where P is a pure function representing the property. In the examples below P is an expression in some variable with a type like this: P: n -> Type++So if n is a natural number variable then P could be something like 2*n + 3.++To use this in our proofs there is the following function in the prelude:++.. code-block:: idris++   ||| Perform substitution in a term according to some equality.+   replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y+   replace Refl prf = prf++Removing the implicits, if we supply an equality (x=y) and a proof of a property of x (P x) then we get a proof of a property of y (P y)++.. code-block:: idris++   > :t replace+   replace : (x = y) -> P x -> P y++So, in the following example, if we supply p1 x which is a proof that x=2 and the equality x=y then we get a proof that y=2.++.. code-block:: idris++   p1: Nat -> Type+   p1 n = (n=2)++   testReplace: (x=y) -> (p1 x) -> (p1 y)+   testReplace a b = replace a b++Rewrite+=======++Similar to 'replace' above but Idris provides a nicer syntax which makes 'rewrite' easier to use in examples like plusReducesR above.++.. code-block:: idris++   rewrite__impl : (P : a -> Type) -> x = y -> P y -> P x+   rewrite__impl p Refl prf = prf++The difference from 'replace' above is nicer syntax and the property p1 is explicitly supplied and it goes in the opposite direction (input and output reversed).++Example: again we supply p1 which is a proof that x=2 and the equality x=y then we get a proof that y=2.++.. code-block:: idris++   p1: Nat -> Type+   p1 x = (x=2)++   testRewrite2: (x=y) -> (p1 y) -> (p1 x)+   testRewrite2 a b = rewrite a in b++We can think of rewrite doing this:++ * Start with a equation x=y and a property P: x -> Type+ * Searches y in P+ * Replaces all occurrences of y with x in P.++That is, we are doing a substitution.++Symmetry and Transitivity+=========================++In addition to 'reflexivity' equality also obeys 'symmetry' and 'transitivity' and these are also included in the prelude:++.. code-block:: idris++   ||| Symmetry of propositional equality+   sym : {left:a} -> {right:b} -> left = right -> right = left+   sym Refl = Refl++   ||| Transitivity of propositional equality+   trans : {a:x} -> {b:y} -> {c:z} -> a = b -> b = c -> a = c+   trans Refl Refl = Refl++Heterogeneous Equality+======================++Also included in the prelude: ++.. code-block:: idris++   ||| Explicit heterogeneous ("John Major") equality. Use this when Idris+   ||| incorrectly chooses homogeneous equality for `(=)`.+   ||| @ a the type of the left side+   ||| @ b the type of the right side+   ||| @ x the left side+   ||| @ y the right side+   (~=~) : (x : a) -> (y : b) -> Type+   (~=~) x y = (x = y)+++

@@ -115,6 +115,24 @@     FFI_C : FFI         FFI_C = MkFFI C_Types String String +Linking foreign code+====================++This is the example of linking C code. ++.. code-block:: idris+    %include C "mylib.h"+    %link C "mylib.o"++Example Makefile++.. code-block:: shell+    DEFAULT: mylib.o main.idr+    	idris main.idr -o executableFile++    clean:+    	rm -f executableFile mylib.o main.ibc+ Foreign calls ============= @@ -336,15 +354,37 @@      CData some_allocating_fun(int arg)     {-        void * data = (void *) malloc(...);+        size_t size = sizeof(...);+        void * data = (void *) malloc(size);         // ...-        return cdata_manage(data, finalizer);+        return cdata_manage(data, size, finalizer);     }      int other_fun(CData cd, int arg)     {         int result = foo(cd->data);         return result;+    }++The ``Raw`` type constructor allows you to access or return a runtime+representation of the value. For instance, if you want to copy a string+generated from C code into an Idris value, you may want to return a+``Raw String``instead of a ``String`` and use ``MKSTR`` or ``MKSTRlen`` to+copy it over.++.. code-block:: idris++    getString : () -> IO (Raw String)+    getString () = foreign FFI_C "get_string" (IO (Raw String))++.. code-block:: cpp++    const VAL get_string ()+    {+        char * c_string = get_string_allocated_with_malloc()+        const VAL idris_string = MKSTR(c_string);+        free(c_string);+        return idris_string     }  FFI implementation

@@ -26,6 +26,7 @@    uniqueness-types    ffi    syntax-guide+   syntax-reference    erasure    ide-protocol    semantic-highlighting

@@ -24,7 +24,7 @@ has two modules ``foo.idr`` and ``bar.idr`` as source files would be written as follows:: -    package foo+    package test      modules = foo, bar 

@@ -390,6 +390,12 @@     partial     covering +Sets explicitly to which extent pattern matching is terminating and/or+exhaustive. A ``partial`` pattern matching makes no assumption. A ``covering``+pattern matching ensures that pattern matching is exhaustive on its clauses.+Furthermore, a ``total`` pattern matching enforces both exhaustivity and+termination of the evaluation of its clauses.+ Implicit Coercion ^^^^^^^^^^^^^^^^^ 

@@ -0,0 +1,422 @@+*****************+Syntax Reference+*****************++Here we present a rough description of Idris' surface syntax as an eBNF grammar.+This presentend grammar may differ from syntax that Idris' parser can handle due to the parser and grammar description not being in sync.++=========+Notation+=========++Grammar shortcut notation::++  ~CHARSEQ = complement of char sequence (i.e. any character except CHARSEQ)+  RULE? = optional rule (i.e. RULE or nothing)+  RULE* = repeated rule (i.e. RULE zero or more times)+  RULE+ = repeated rule with at least one match (i.e. RULE one or more times)+  RULE! = invalid rule (i.e. rule that is not valid in context, report meaningful error in case)+  RULE{n} = rule repeated n times+++=============+Main Grammar+=============++.. productionlist::+   ModuleHeader : `DocComment_t`? "module" `Identifier_t` ";"? ;+   Import       : "import" `Identifier_t` ";"? ;+   Prog         : `Decl`* `EOF`;+   Decl         : `DeclP`+                : | `Using`+                : | `Params`+                : | `Mutual`+                : | `Namespace`+                : | `Interface`+                : | `Implementation`+                : | `DSL`+                : | `Directive`+                : | `Provider`+                : | `Transform`+                : | `Import`!+                : | `RunElabDecl` ;+   DeclP : `Fixity`+         : | `FunDecl`+         : | `Data`+         : | `Record`+         : | `SyntaxDecl` ;+++--------------------+Syntax Declarations+--------------------++.. productionlist::+   SyntaxDecl : `SyntaxRule` ;+   SyntaxRuleOpts : "term" | "pattern" ;+   SyntaxRule : `SyntaxRuleOpts`? "syntax" `SyntaxSym`+ "=" `TypeExpr` `Terminator`;+   SyntaxSym :   '[' `Name_t` ']'+             : |  '{' `Name_t` '}'+             : |  `Name_t`+             : |  `StringLiteral_t`;+   SyntaxSym :    '[' `Name_t` ']'+             : |  '{' `Name_t` '}'+             : |  `Name_t`+             : |  `StringLiteral_t`;++----------+Functions+----------++.. productionlist::+   FunDecl : `FunDeclP`;+   FunDeclP : `DocComment_t`? `FnOpts`* `Accessibility`? `FnOpts`* `FnName` `TypeSig` `Terminator`+            : | `Postulate`+            : | `Pattern`+            : | `CAF` ;+   FnOpts : `FnOpt`* `Accessibility` `FnOpt`* ;+   FnOpt :   'total'+         : | 'partial'+         : | 'covering'+         : | 'implicit'+         : | '%' 'no_implicit'+         : | '%' 'assert_total'+         : | '%' 'error_handler'+         : | '%' 'reflection'+         : | '%' 'specialise' '[' `NameTimesList`? ']' ;+   NameTimes : `FnName` `Natural`?;+   NameTimesList : `NameTimes` | `NameTimes` ',' `NameTimesList` ;+   Postulate : `DocComment_t`? 'postulate' `FnOpts`* `Accesibility`? `FnOpts`* `FnName` `TypeSig` `Terminator` ;++--------------------+Blocks & Namespaces+--------------------++.. productionlist::+  Using : 'using' '(' `UsingDeclList` ')' `OpenBlock` `Decl`* `CloseBlock` ;+  UsingDeclList : `UsingDeclListP` | `NameList TypeSig`;+  UsingDeclListP : `UsingDecl` | `UsingDecl` ',' `UsingDeclListP` ;+  NameList : `Name` | `Name` ',' `NameList` ;+  UsingDecl : `FnName` `TypeSig` | `FnName` `FnName`+ ;+  Params : 'parameters' '(' `TypeDeclList` ')' `OpenBlock` `Decl`* `CloseBlock`;+  Mutual : 'mutual' `OpenBlock` `Decl`* `CloseBlock` ;+  Namespace : 'namespace' `identifier` `OpenBlock` `Decl`+ `CloseBlock` ;++----------------------------+Interfaces & Implementation+----------------------------++.. productionlist::+  ImplementationBlock : 'where' `OpenBlock` `FnDecl`* `CloseBlock` ;+  MethodOrImplementation : `FnDecl` | `Implementation`;+  InterfaceBlock : 'where' `OpenBlock` `Constructor`? `MethodOrImplementation`* `CloseBlock` ;+  InterfaceArgument : `Name` | '(' `Name` ':' `Expr` ')';+  Interface ::= `DocComment_t`? `Accessibility`? 'interface' `ConstraintList`? `Name` `InterfaceArgument`* `InterfaceBlock`?;+  Implementation : `DocComment_t`? 'implementation' `ImplementationName`? `ConstraintList`? `Name` `SimpleExpr`* `ImplementationBlock`? ;+  ImplementationName : '[' `Name` ']';+++-------+Bodies+-------++.. productionlist::+  Pattern : `Clause`;+  CAF : 'let' `FnName` '=' `Expr` `Terminator`;+  ArgExpr : `HSimpleExpr` | "In Pattern External (User-defined) Expression";+  RHS :    '='             `Expr`+      : | '?='  `RHSName`? `Expr`+      : |  `Impossible` ;+  RHSName : '{' `FnName` '}' ;+  RHSOrWithBlock : `RHS` `WhereOrTerminator`+                 : | 'with' `SimpleExpr` `OpenBlock` `FnDecl`+ `CloseBlock`;+  Clause :   `WExpr`+ `RHSOrWithBlock`+         : | `SimpleExpr` '<=='  `FnName` `RHS` `WhereOrTerminator`+         : | `ArgExpr` `Operator` `ArgExpr` `WExpr`* `RHSOrWithBlock` {- Except "=" and "?=" operators to avoid ambiguity -}+         : | `FnName` `ConstraintArg`* `ImplicitOrArgExpr`*    `WExpr`* `RHSOrWithBlock`;+  ImplicitOrArgExpr ::= `ImplicitArg` | `ArgExpr`;+  WhereOrTerminator ::= `WhereBlock` | `Terminator`;+  WExpr ::= '|' `Expr`';+  WhereBlock : 'where' `OpenBlock` `Decl`+ `CloseBlock`;++----------+Directives+----------++.. productionlist::+  Codegen: 'C'+         : | 'Java'+         : | 'JavaScript'+         : | 'Node'+         : | 'LLVM'+         : | 'Bytecode' ;+  StringList : `String` | `String` ',' `StringList` ;+  Directive : '%' `DirectiveP`;+  DirectiveP :   'lib'            `CodeGen` `String_t`+             : | 'link'           `CodeGen` `String_t`+             : | 'flag'           `CodeGen` `String_t`+             : | 'include'        `CodeGen` `String_t`+             : | 'hide'           `Name`+             : | 'freeze'         `Name`+             : | 'thaw'           `Name`+             : | 'access'         `Accessibility`+             : | 'default'        `Totality`+             : | 'logging'        `Natural`+             : | 'dynamic'        `StringList`+             : | 'name'           `Name` `NameList`+             : | 'error_handlers' `Name` `NameList`+             : | 'language'       'TypeProviders'+             : | 'language'       'ErrorReflection'+             : | 'deprecated' `Name` `String`+             : | 'fragile'    `Name` `Reason` ;+  LangExt :   "TypeProviders"+          : | "ErrorReflection"+          : | "UniquenessTypes"+          : | "LinearTypes"+          : | "DSLNotation"+          : | "ElabReflection"+          : | "FirstClassReflection" ;+  Totality : 'partial' | 'total' | 'covering'+  Provider : `DocComment_t`? '%' 'provide' `Provider_What`? '(' `FnName` `TypeSig` ')' 'with' `Expr`;+  ProviderWhat : 'proof' | 'term' | 'type' | 'postulate'+  Transform : '%' 'transform' `Expr` '==>' `Expr`;+  RunElabDecl : '%' 'runElab' `Expr`;+++===========+Expressions+===========++.. productionlist::+  FullExpr : `Expr` `EOF_t` ;+  Expr     : `Pi` ;+  OpExpr   : "Expression Parser with Operators based on ExprP" ;+  ExprP    : "External (User-defined) Syntax" |  `InternalExpr` ;+  InternalExpr : `UnifyLog`+               : | `RecordType`+               : | `SimpleExpr`+               : | `Lambda`+               : | `QuoteGoal`+               : | `Let`+               : | `If`+               : | `RewriteTerm`+               : | `CaseExpr`+               : | `DoBlock`+               : | `App` ;++-------+Bodies+-------++.. productionlist::+  Impossible : `impossible` ;+  CaseExpr : "case" `Expr` "of" `OpenBlock` `CaseOption`+ `CloseBlock` ;+  CaseOption : `Expr` (`Impossible` | "=>" `Expr`) `Terminator` ;+  ProofExpr : "proof" `OpenBlock` `Tactic'`* `CloseBlock` ;+  TacticsExpr : "tactics" `OpenBlock` `Tactic'`* `CloseBlock` ;+  SimpleExpr : "External (User-defined) Simple Expression"+             : | "?" `Name`+             : | "%" "implementation"+             : | "Refl" ("{" `Expr` "}")?+             : | `ProofExpr`+             : | `TacticsExpr`+             : | `FnName`+             : | `Idiom`+             : | `List`+             : | `Alt`+             : | `Bracketed`+             : | `Constant`+             : | `Type`+             : | "Void"+             : | `Quasiquote`+             : | `NameQuote`+             : | `Unquote`+             : | "_" ;+  Bracketed : "(" `BracketedP` ;+  BracketedP : ")"+             : | `Expr` ")"+             : | `ExprList` ")"+             : | `DependentPair` ")"+             : | `Operator` `Expr` ")"+             : | `Expr` `Operator` ")" ;+  Alt : "(|" `Expr_List` "|)" ;+  Expr_List : `Expr'` | `Expr'` "," `Expr_List` ;+  HSimpleExpr : "." `SimpleExpr` | `SimpleExpr` ;+  UnifyLog : "%" "unifyLog" `SimpleExpr` ;+  RunTactics : "%" "runElab" `SimpleExpr` ;+  Disamb : "with" `NameList` `Expr` ;+  NoImplicits : "%" "noImplicits" `SimpleExpr` ;+  App : "mkForeign" `Arg` `Arg`*+      : | `MatchApp`+      : | `SimpleExpr` `Arg`* ;+  MatchApp : `SimpleExpr` "<==" `FnName` ;+  Arg :` ImplicitArg` | `ConstraintArg` | `SimpleExpr` ;+  ImplicitArg : "{" `Name` ("=" `Expr`)? "}" ;+  ConstraintArg : "@{" `Expr` "}" ;+  Quasiquote : "`(" `Expr` ")" ;+  Unquote : "," `Expr` ;+  RecordType : "record" "{" `FieldTypeList` "}" ;+  FieldTypeList : `FieldType` | `FieldType` "," `FieldTypeList` ;+  FieldType : `FnName` "=" `Expr` ;+  TypeSig : ":" `Expr` ;+  TypeExpr : `ConstraintList`? `Expr` ;+  Lambda : "\\" `TypeOptDeclList` `LambdaTail`+         : | "\\" `SimpleExprList`  `LambdaTail` ;+  SimpleExprList : `SimpleExpr` | `SimpleExpr` "," `SimpleExprList` ;+  LambdaTail : `Impossible` | "=>" `Expr` ;+  RewriteTerm : "rewrite" `Expr` ("==>" `Expr`)? "in" `Expr` ;+  RigCount: "1" : "0" ;+  Let : "let" `Name` `TypeSig`"? "=" `Expr`  "in" `Expr`+      : | "let" `Expr'`            "=" `Expr'` "in" `Expr` ;+  TypeSig' : ":" `Expr'` ;+  If : "if" `Expr` "then" `Expr` "else" `Expr` ;+  QuoteGoal : "quoteGoal" `Name` "by" `Expr` "in" `Expr` ;++----+Pies+----++.. productionlist::+  Pi : `PiOpts` `Static`? `PiP` ;+  PiP : `OpExpr` ("->" `Pi`)?+      : | "(" `TypeDeclList`           ")"            "->" `Pi`+      : | "{" `TypeDeclList`           "}"            "->" `Pi`+      : | "{" "auto"    `TypeDeclList` "}"            "->" `Pi`+      : | "{" "default" `SimpleExpr` `TypeDeclList` "}" "->" `Pi` ;+  PiOpts : "."? ;+  ConstraintList : "(" `Expr_List` ")" "=>"+                 : | `Expr`              "=>" ;+  TypeDeclList : `FunctionSignatureList`+               : | `NameList` `TypeSig` ;+  FunctionSignatureList : `Name` `TypeSig`+                        : | `Name` `TypeSig` "," `FunctionSignatureList` ;+  TypeOptDeclList : `NameOrPlaceholder` `TypeSig`?+                  : | `NameOrPlaceholder` `TypeSig`? "," `TypeOptDeclList` ;+  NameOrPlaceHolder : `Name` : "_" ;+  ListExpr : "[" "]" | "[" `Expr` "|" `DoList` "]" | "[" `ExprList` "]" ;+  ExprList : `Expr` | `Expr` "," `ExprList` ;+++-------------------+Do Blocks & Idioms+-------------------++.. productionlist::+  DoList : `Do` : `Do` "," `DoList` ;+  Do' : `Do` `KeepTerminator` ;+  DoBlock : "do" `OpenBlock` `Do'`+ `CloseBlock` ;+  Do : "let" `Name`  `TypeSig`"?      "=" `Expr`+     : | "let" `Expr'`                  "=" `Expr`+     : | "rewrite" `Expr`+     : | `Name`  "<-" `Expr`+     : | `Expr'` "<-" `Expr`+     : | `Expr` ;+  Idiom : "[|" `Expr` "|]" ;+++----------+Constants+----------++.. productionlist::+  Constant : | "Integer"+           : | "Int"+           : | "Char"+           : | "Double"+           : | "String"+           : | "Bits8"+           : | "Bits16"+           : | "Bits32"+           : | "Bits64"+           : | `Float_t`+           : | `Natural_t`+           : | `VerbatimString_t`+           : | `String_t`+           : | `Char_t` ;+  VerbatimString_t : "\"\"\"" ~"\"\"\"" "\""* "\"\"\"" ;++-------+Tactics+-------++.. productionlist::+  Tactic : "intro" `NameList`?+         : |  "intros"+         : |  "refine"      `Name` `Imp`++         : |  "mrefine"     `Name`+         : |  "rewrite"     `Expr`+         : |  "induction"   `Expr`+         : |  "equiv"       `Expr`+         : |  "let"         `Name` ":" `Expr'` "=" `Expr`+         : |  "let"         `Name`            "=" `Expr`+         : |  "focus"       `Name`+         : |  "exact"       `Expr`+         : |  "applyTactic" `Expr`+         : |  "reflect"     `Expr`+         : |  "fill"        `Expr`+         : |  "try"         `Tactic` "|" `Tactic`+         : |  "{" `TacticSeq` "}"+         : |  "compute"+         : |  "trivial"+         : |  "solve"+         : |  "attack"+         : |  "state"+         : |  "term"+         : |  "undo"+         : |  "qed"+         : |  "abandon"+         : |  ":" "q" ;+  TacticSeq : `Tactic` ";" `Tactic` | `Tactic` ";" `TacticSeq` ;++----+Misc+----++.. productionlist::+  Imp : "?" | "_" ;+  Static : "%static" ;++=====+Data+=====++.. productionlist::+  Record : `DocComment` `Accessibility`? "record" `FnName` `TypeSig` "where" `OpenBlock` `Constructor` `KeepTerminator` `CloseBlock`;+  DataI : "data" | "codata";+  Data : `DocComment`? `Accessibility`? `DataI` `FnName` `TypeSig` `ExplicitTypeDataRest`?+       : `DocComment`? `Accessibility`? `DataI` `FnName` `Name`* `DataRest`? ;+  Constructor': `Constructor` `KeepTerminator` ;+  ExplicitTypeDataRest : "where" `OpenBlock` `Constructor'`* `CloseBlock`;+  DataRest : "=" `SimpleConstructorList` `Terminator` | "where"!;+  SimpleConstructorList : `SimpleConstructor` | `SimpleConstructor` "|" `SimpleConstructorList`;+  Constructor : `DocComment`? `FnName` `TypeSig`;+  SimpleConstructor : `FnName` `SimpleExpr`* `DocComment`?;+  DSL : "dsl" `FnName` `OpenBlock` `Overload'`+ `CloseBlock`;+  OverloadIdentifier : "let" | `Identifier`;+  Overload : `OverloadIdentifier` "=" `Expr`;+++=========+Operators+=========++.. productionlist::+  BacktickOperator: `Name` ;+  OperatorName: `SymbolicOperator` : `BacktickOperator` ;+  OperatorFront: "(" "=" ")" | (`Identifier_t` ".")? "(" `Operator_t` ")" ;+  FnName: `Name` | `OperatorFront`;+  Fixity: `FixityType` `Natural_t` `OperatorList` `Terminator`;+  FixityType: "infixl" | "infixr" | "infix" | "prefix";+++==============+Documentation+==============++.. productionlist::+  SingleLineComment_t: "--" ~`EOL_t`* `EOL_t` ;+  MultiLineComment_t: "{" ..  "}" | "{ -" `InCommentChars_t` ;+  InCommentChars_t : "- }" | `MultiLineComment_t` `InCommentChars_t` | ~"- }"+ `InCommentChars_t`;+  DocComment_t : `DocCommentLine` (`ArgCommentLine` `DocCommentLine`*)* ;+  DocCommentLine : "|||" ~`EOL_t`* `EOL_t` ;+  ArgCommentLine : "|||" "@" ~`EOL_t`* `EOL_t` ;

@@ -350,7 +350,7 @@  To implement ``Sockets`` in ``IO``, we'll begin by giving a concrete type for ``Sock``. We can use the raw sockets API (implemented in-``Network.Sockeet``) for this, and use a ``Socket`` stored in a ``State``, no+``Network.Socket``) for this, and use a ``Socket`` stored in a ``State``, no matter what abstract state the socket is in:  .. code-block:: idris

@@ -164,7 +164,7 @@           lift $ putStrLn ("var = " ++ show !(read var))           delete var -The ``lift`` function allows us to use funtions from the underlying+The ``lift`` function allows us to use functions from the underlying computation context (``IO`` here) directly. Again, we'll see the exact type of ``lift`` shortly. 

@@ -11,7 +11,7 @@    questions on the mailing list.  -  The IRC channel ``#idris``, on-   `chat.freenode.net <http://chat.freenode.net>`__.+   `webchat.freenode.net <https://webchat.freenode.net/>`__.  - The wiki (https://github.com/idris-lang/Idris-dev/wiki/) has further    user provided information, in particular:

@@ -30,7 +30,7 @@     interpTy : Ty -> Type     interpTy TyInt       = Integer     interpTy TyBool      = Bool-    interpTy (TyFun A T) = interpTy A -> interpTy T+    interpTy (TyFun a t) = interpTy a -> interpTy t  We're going to define a representation of our language in such a way that only well-typed programs can be represented. We'll index the

@@ -6,7 +6,7 @@  Idris includes a simple build system for building packages and executables from a named package description file. These files can be used with the-Idris compiler to manage the development process .+Idris compiler to manage the development process.  Package Descriptions ====================

@@ -153,5 +153,4 @@  .. [1] Conor McBride and James McKinna. 2004. The view from the        left. J. Funct. Program. 14, 1 (January 2004),-       69-111. DOI=10.1017/S0956796803004829-       http://dx.doi.org/10.1017/S0956796803004829ñ+       69-111. https://doi.org/10.1017/S0956796803004829

@@ -1,5 +1,5 @@ Name:           idris-Version:        1.3.1+Version:        1.3.2 License:        BSD3 License-file:   LICENSE Author:         Edwin Brady@@ -100,7 +100,7 @@  custom-setup   setup-depends:-    Cabal >= 1.10 && <2.3,+    Cabal >= 1.10 && <2.5,     base  >= 4 && <5,     directory,     filepath,@@ -270,7 +270,7 @@                 , BuildFlags_idris    Build-depends:  base >=4 && <5-                , aeson >= 0.6 && < 1.4+                , aeson >= 0.6 && < 1.5                 , annotated-wl-pprint >= 0.7 && < 0.8                 , ansi-terminal < 0.9                 , ansi-wl-pprint < 0.7@@ -281,18 +281,19 @@                 , blaze-markup >= 0.5.2.1 && < 0.9                 , bytestring < 0.11                 , cheapskate >= 0.1.1 && < 0.2-                , code-page >= 0.1 && < 0.2-                , containers >= 0.5 && < 0.6+                , code-page >= 0.1 && < 0.3+                , containers >= 0.5 && < 0.7                 , deepseq < 1.5                 , directory >= 1.2.2.0 && < 1.2.3.0 || > 1.2.3.0                 , filepath < 1.5                 , fingertree >= 0.1.4.1 && < 0.2                 , haskeline >= 0.7 && < 0.8                 , ieee754 >= 0.7 && < 0.9-                , megaparsec >= 6.2 && < 7+                , megaparsec >= 7.0.4 && < 8                 , mtl >= 2.1 && < 2.3-                , network < 2.8+                , network >= 2.7 && < 2.9                 , optparse-applicative >= 0.13 && < 0.15+                , parser-combinators >= 1.0.0                 , pretty < 1.2                 , process < 1.7                 , regex-tdfa >= 1.2@@ -307,7 +308,7 @@                 , utf8-string < 1.1                 , vector < 0.13                 , vector-binary-instances < 0.3-                , zip-archive > 0.2.3.5 && < 0.4+                , zip-archive > 0.2.3.5 && < 0.5                 , fsnotify >= 0.2 && < 2.2                 , async < 2.3 

@@ -7,5 +7,9 @@     }     return ""; };-$JSRTS.prim_writeStr = function (x) { return console.log(x) }++$JSRTS.prim_writeStr = function (x) { return console.log(x) };+ $JSRTS.prim_readStr = function () { return prompt('Prelude.getLine') };++$JSRTS.die = function (message) { throw new Error(message) };

@@ -1,5 +1,7 @@ $JSRTS.os = require('os');+ $JSRTS.fs = require('fs');+ $JSRTS.prim_systemInfo = function (index) {     switch (index) {         case 0:@@ -9,10 +11,12 @@     }     return ""; };-$JSRTS.prim_writeStr = function (x) { return process.stdout.write(x) }++$JSRTS.prim_writeStr = function (x) { return process.stdout.write(x) };+ $JSRTS.prim_readStr = function () {     var ret = '';-    var b = new Buffer(1024);+    var b = Buffer.alloc(1024);     var i = 0;     while (true) {         $JSRTS.fs.readSync(0, b, i, 1)@@ -22,10 +26,15 @@         }         i++;         if (i == b.length) {-            var nb = new Buffer(b.length * 2);+            var nb = Buffer.alloc(b.length * 2);             b.copy(nb)             b = nb;         }     }     return ret;+};++$JSRTS.die = function (message) {+    console.error(message);+    process.exit(-1); };

@@ -7,6 +7,7 @@ import Control.Monad.Trans  %access public export+%default total  interface Catchable (m : Type -> Type) t | m where     throw : t -> m a

@@ -29,3 +29,9 @@   toNat (Id x) = toNat x   fromNat n = Id $ fromNat n   pred (Id n) = Id $ pred n++(Semigroup a) => Semigroup (Identity a) where+  (<+>) x y = Id (runIdentity x <+> runIdentity y)++(Monoid a) => Monoid (Identity a) where+  neutral = Id (neutral)

@@ -64,3 +64,6 @@ ||| The Writer monad itself. See the MonadWriter interface Writer : Type -> Type -> Type Writer w a = WriterT w Identity a++runWriter : Writer w a -> (a, w)+runWriter = runIdentity . runWriterT

@@ -1,5 +1,7 @@ module Data.IORef +%default total+ ||| A mutable variable in the IO monad. export data IORef a = MkIORef a

@@ -45,36 +45,64 @@ --------------------------------------------------------------------------------  ||| All but the first element of the vector+|||+||| ```idris example+||| tail [1,2,3,4]+||| ``` tail : Vect (S len) elem -> Vect len elem tail (x::xs) = xs  ||| Only the first element of the vector+|||+||| ```idris example+||| head [1,2,3,4]+||| ``` head : Vect (S len) elem -> elem head (x::xs) = x  ||| The last element of the vector+|||+||| ```idris example+||| last [1,2,3,4]+||| ``` last : Vect (S len) elem -> elem last (x::[])    = x last (x::y::ys) = last $ y::ys  ||| All but the last element of the vector+|||+||| ```idris example+||| init [1,2,3,4]+||| ``` init : Vect (S len) elem -> Vect len elem init (x::[])    = [] init (x::y::ys) = x :: init (y::ys)  ||| Extract a particular element from a vector+|||+||| ```idris example+||| index 1 [1,2,3,4]+||| ``` index : Fin len -> Vect len elem -> elem index FZ     (x::xs) = x index (FS k) (x::xs) = index k xs   ||| Insert an element at a particular index+|||+||| ```idris example+||| insertAt 1 8 [1,2,3,4]+||| ``` insertAt : Fin (S len) -> elem -> Vect len elem -> Vect (S len) elem insertAt FZ     y xs      = y :: xs insertAt (FS k) y (x::xs) = x :: insertAt k y xs insertAt (FS k) y []      = absurd k  ||| Construct a new vector consisting of all but the indicated element+|||+||| ```idris example+||| deleteAt 1 [1,2,3,4]+||| ``` deleteAt : Fin (S len) -> Vect (S len) elem -> Vect len elem deleteAt             FZ     (x::xs) = xs deleteAt {len = S m} (FS k) (x::xs) = x :: deleteAt k xs@@ -82,6 +110,10 @@ deleteAt             _      []      impossible  ||| Replace an element at a particlar index with another+|||+||| ```idris example+||| replaceAt 1 8 [1,2,3,4]+||| ``` replaceAt : Fin len -> elem -> Vect len elem -> Vect len elem replaceAt FZ     y (x::xs) = y :: xs replaceAt (FS k) y (x::xs) = x :: replaceAt k y xs@@ -90,6 +122,10 @@ ||| @ i the index to replace at ||| @ f the update function ||| @ xs the vector to replace in+|||+||| ```idris example+||| updateAt 1 (+10) [1,2,3,4]+||| ``` updateAt : (i : Fin len) -> (f : elem -> elem) -> (xs : Vect len elem) -> Vect len elem updateAt FZ     f (x::xs) = f x :: xs updateAt (FS k) f (x::xs) = x :: updateAt k f xs@@ -100,20 +136,54 @@  ||| Get the first n elements of a Vect ||| @ n the number of elements to take+|||+||| ```idris example+||| take 2 [1,2,3,4]+||| ``` take : (n : Nat) -> Vect (n + m) elem -> Vect n elem take Z     xs        = [] take (S k) (x :: xs) = x :: take k xs  ||| Remove the first n elements of a Vect ||| @ n the number of elements to remove+|||+||| ```idris example+||| drop 2 [1,2,3,4]+||| ``` drop : (n : Nat) -> Vect (n + m) elem -> Vect m elem drop Z     xs        = xs drop (S k) (x :: xs) = drop k xs +||| Take up to the first n elements of a Vect if they exist.+||| @ n the maximum number of elements to take+|||+||| ```idris example+||| takeUpto 10 [1,2,3,4]+||| ```+takeUpto : (x : Nat) -> Vect n elem -> Vect (minimum x n) elem+takeUpto Z ys = []+takeUpto x [] = rewrite minimumZeroZeroLeft x in []+takeUpto (S x) (y::ys) = y :: takeUpto x ys++||| Drop up to the first n elements of a Vect if they exist.+||| @ n the maximum number of elements to remove.+|||+||| ```idris example+||| dropUpto 10 [1,2,3,4]+||| ```+dropUpto : (x : Nat) -> Vect n elem -> Vect (n `minus` minimum x n) elem+dropUpto Z ys {n} = rewrite minusZeroRight n in ys+dropUpto x [] = []+dropUpto (S x) (y :: ys) = dropUpto x ys+ ||| Take the longest prefix of a Vect such that all elements satisfy some ||| Boolean predicate. ||| ||| @ p the predicate+|||+||| ```idris example+||| takeWhile (<3) [1,2,3,4]+||| ``` takeWhile : (p : elem -> Bool) -> Vect len elem -> (q ** Vect q elem) takeWhile p []      = (_ ** []) takeWhile p (x::xs) =@@ -127,6 +197,10 @@ ||| Boolean predicate. ||| ||| @ p the predicate+|||+||| ```idris example+||| dropWhile (<3) [1,2,3,4]+||| ``` dropWhile : (p : elem -> Bool) -> Vect len elem -> (q ** Vect q elem) dropWhile p [] = (_ ** []) dropWhile p (x::xs) =@@ -140,6 +214,10 @@ --------------------------------------------------------------------------------  ||| Reverse the order of the elements of a vector+|||+||| ```idris example+||| reverse [1,2,3,4]+||| ``` reverse : Vect len elem -> Vect len elem reverse xs = go [] xs   where go : Vect n elem -> Vect m elem -> Vect (n+m) elem@@ -150,6 +228,10 @@ ||| Alternate an element between the other elements of a vector ||| @ sep the element to intersperse ||| @ xs the vector to separate with `sep`+|||+||| ```idris example+||| intersperse 0 [1,2,3,4]+||| ``` intersperse : (sep : elem) -> (xs : Vect len elem) -> Vect (len + pred len) elem intersperse sep []      = [] intersperse sep (x::xs) = x :: intersperse' sep xs@@ -174,6 +256,10 @@ ||| Convert a list to a vector. ||| ||| The length of the list should be statically known.+|||+||| ```idris example+||| fromList [1,2,3,4]+||| ``` fromList : (l : List elem) -> Vect (length l) elem fromList l =   rewrite (sym $ plusZeroRightNeutral (length l)) in@@ -184,6 +270,10 @@ --------------------------------------------------------------------------------  ||| Append two vectors+|||+||| ```idris example+||| [1,2,3,4] ++ [5,6]+||| ``` (++) : (xs : Vect m elem) -> (ys : Vect n elem) -> Vect (m + n) elem (++) []      ys = ys (++) (x::xs) ys = x :: xs ++ ys@@ -192,11 +282,19 @@ ||| ||| @ len the number of times to repeat it ||| @ x the value to repeat+|||+||| ```idris example+||| replicate 4 1+||| ``` replicate : (len : Nat) -> (x : elem) -> Vect len elem replicate Z     x = [] replicate (S k) x = x :: replicate k x  ||| Merge two ordered vectors+|||+||| ```idris example+||| mergeBy compare (fromList [1,3,5]) (fromList [2,3,4,5,6])+||| ``` mergeBy : (elem -> elem -> Ordering) -> (xs : Vect n elem) -> (ys : Vect m elem) -> Vect (n + m) elem mergeBy order [] [] = [] mergeBy order [] (x :: xs) = x :: xs@@ -220,30 +318,54 @@ ||| @ f the function to combine elements with ||| @ xs the first vector of elements ||| @ ys the second vector of elements+|||+||| ```idris example+||| zipWith (+) (fromList [1,2,3,4]) (fromList [5,6,7,8])+||| ``` zipWith : (f : a -> b -> c) -> (xs : Vect n a) -> (ys : Vect n b) -> Vect n c zipWith f []      []      = [] zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys  ||| Combine three equal-length vectors into a vector with some function+|||+||| ```idris example+||| zipWith3 (\x,y,z => x+y+z) (fromList [1,2,3,4]) (fromList [5,6,7,8]) (fromList [1,1,1,1])+||| ``` zipWith3 : (a -> b -> c -> d) -> (xs : Vect n a) -> (ys : Vect n b) -> (zs : Vect n c) -> Vect n d zipWith3 f []      []      []      = [] zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs  ||| Combine two equal-length vectors pairwise+|||+||| ```idris example+||| zip (fromList [1,2,3,4]) (fromList [1,2,3,4])+||| ``` zip : (xs : Vect n a) -> (ys : Vect n b) -> Vect n (a, b) zip = zipWith (\x,y => (x,y))  ||| Combine three equal-length vectors elementwise into a vector of tuples+|||+||| ```idris example+||| zip3 (fromList [1,2,3,4]) (fromList [1,2,3,4]) (fromList [1,2,3,4])+||| ``` zip3 : (xs : Vect n a) -> (ys : Vect n b) -> (zs : Vect n c) -> Vect n (a, b, c) zip3 = zipWith3 (\x,y,z => (x,y,z))  ||| Convert a vector of pairs to a pair of vectors+|||+||| ```idris example+||| unzip (fromList [(1,2), (1,2)])+||| ``` unzip : (xs : Vect n (a, b)) -> (Vect n a, Vect n b) unzip []           = ([], []) unzip ((l, r)::xs) with (unzip xs)   | (lefts, rights) = (l::lefts, r::rights)  ||| Convert a vector of three-tuples to a triplet of vectors+|||+||| ```idris example+||| unzip3 (fromList [(1,2,3), (1,2,3)])+||| ``` unzip3 : (xs : Vect n (a, b, c)) -> (Vect n a, Vect n b, Vect n c) unzip3 []            = ([], [], []) unzip3 ((l,c,r)::xs) with (unzip3 xs)@@ -285,6 +407,10 @@ ||| ||| @ f the partial function (expressed by returning `Maybe`) ||| @ xs the vector to check for results+|||+||| ```idris example+||| mapMaybe ((find (=='a')) . unpack) (fromList ["abc","ade","bgh","xyz"])+||| ``` mapMaybe : (f : a -> Maybe b) -> (xs : Vect len a) -> (m : Nat ** Vect m b) mapMaybe f []      = (_ ** []) mapMaybe f (x::xs) =@@ -309,15 +435,28 @@ --------------------------------------------------------------------------------  ||| Flatten a vector of equal-length vectors+|||+||| ```idris example+||| concat [[1,2,3], [4,5,6]]+||| ``` concat : (xss : Vect m (Vect n elem)) -> Vect (m * n) elem concat []      = [] concat (v::vs) = v ++ concat vs  ||| Foldr without seeding the accumulator+|||+||| ```idris example+||| foldr1 (-) (fromList [1,2,3])+||| ``` foldr1 : (t -> t -> t) -> Vect (S n) t -> t-foldr1 f (x::xs) = foldr f x xs+foldr1 f [x]        = x+foldr1 f (x::y::xs) = f x (foldr1 f (y::xs))  ||| Foldl without seeding the accumulator+|||+||| ```idris example+||| foldl1 (-) (fromList [1,2,3])+||| ``` foldl1 : (t -> t -> t) -> Vect (S n) t -> t foldl1 f (x::xs) = foldl f x xs @@ -327,6 +466,10 @@  ||| The scanl function is similar to foldl, but returns all the intermediate ||| accumulator states in the form of a vector.+|||+||| ```idris example+||| scanl (-) 0 (fromList [1,2,3])+||| ``` scanl : (res -> elem -> res) -> res -> Vect len elem -> Vect (S len) res scanl f q []      = [q] scanl f q (x::xs) = q :: scanl f (f q x) xs@@ -335,6 +478,10 @@ ||| starting value. ||| It assumes the first element of the vector to be the starting value and then ||| starts the fold with the element following it.+|||+||| ```idris example+||| scanl1 (-) (fromList [1,2,3])+||| ``` scanl1 : (elem -> elem -> elem) -> Vect len elem -> Vect len elem scanl1 f [] = [] scanl1 f (x::xs) = scanl f x xs@@ -347,6 +494,10 @@ ||| @ p the equality test ||| @ e the item to search for ||| @ xs the vector to search in+|||+||| ```idris example+||| elemBy (==) 2 [1,2,3,4]+||| ``` elemBy : (p : elem -> elem -> Bool) -> (e : elem) -> (xs : Vect len elem) -> Bool elemBy p e []      = False elemBy p e (x::xs) = p e x || elemBy p e xs@@ -354,17 +505,29 @@ ||| Use the default Boolean equality on elements to search for an item ||| @ x what to search for ||| @ xs where to search+|||+||| ```idris example+||| elem 3 [1,2,3,4]+||| ``` elem : Eq elem => (x : elem) -> (xs : Vect len elem) -> Bool elem = elemBy (==)  ||| Find the association of some key with a user-provided comparison ||| @ p the comparison operator for keys (True if they match) ||| @ e the key to look for+|||+||| ```idris example+||| lookupBy (==) 2 [(1, 'a'), (2, 'b'), (3, 'c')]+||| ``` lookupBy : (p : key -> key -> Bool) -> (e : key) -> (xs : Vect n (key, val)) -> Maybe val lookupBy p e []           = Nothing lookupBy p e ((l, r)::xs) = if p e l then Just r else lookupBy p e xs  ||| Find the assocation of some key using the default Boolean equality test+|||+||| ```idris example+||| lookup 3 [(1, 'a'), (2, 'b'), (3, 'c')]+||| ``` lookup : Eq key => key -> Vect n (key, val) -> Maybe val lookup = lookupBy (==) @@ -372,11 +535,19 @@ ||| @ p the comparison operator ||| @ elems the vector to search ||| @ xs what to search for+|||+||| ```idris example+||| hasAnyBy (==) [2,5] [1,2,3,4]+||| ``` hasAnyBy : (p : elem -> elem -> Bool) -> (elems : Vect m elem) -> (xs : Vect len elem) -> Bool hasAnyBy p elems []      = False hasAnyBy p elems (x::xs) = elemBy p x elems || hasAnyBy p elems xs  ||| Check if any element of xs is found in elems using the default Boolean equality test+|||+||| ```idris example+||| hasAny [2,5] [1,2,3,4]+||| ``` hasAny : Eq elem => Vect m elem -> Vect len elem -> Bool hasAny = hasAnyBy (==) @@ -386,30 +557,62 @@  ||| Find the first element of the vector that satisfies some test ||| @ p the test to satisfy+|||+||| ```idris example+||| find (== 3) [1,2,3,4]+||| ``` find : (p : elem -> Bool) -> (xs : Vect len elem) -> Maybe elem find p []      = Nothing find p (x::xs) = if p x then Just x else find p xs  ||| Find the index of the first element of the vector that satisfies some test+|||+||| ```idris example+||| findIndex (== 3) [1,2,3,4]+||| ``` findIndex : (elem -> Bool) -> Vect len elem -> Maybe (Fin len) findIndex p []        = Nothing findIndex p (x :: xs) = if p x then Just 0 else map FS (findIndex p xs)  ||| Find the indices of all elements that satisfy some test+|||+||| ```idris example+||| findIndices (< 3) [1,2,3,4]+||| ``` findIndices : (elem -> Bool) -> Vect m elem -> List (Fin m) findIndices p []        = [] findIndices p (x :: xs) = let is = map FS $ findIndices p xs                            in if p x then 0 :: is else is +||| Find the index of the first element of the vector that satisfies some test+|||+||| ```idris example+||| elemIndexBy (==) 3 [1,2,3,4]+||| ``` elemIndexBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> Maybe (Fin m) elemIndexBy p e = findIndex $ p e +||| Find the index of the first element of the vector equal to the given one.+|||+||| ```idris example+||| elemIndex 3 [1,2,3,4]+||| ``` elemIndex : Eq elem => elem -> Vect m elem -> Maybe (Fin m) elemIndex = elemIndexBy (==) +||| Find the indices of all elements that satisfy some test+|||+||| ```idris example+||| elemIndicesBy (<=) 3 [1,2,3,4]+||| ``` elemIndicesBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> List (Fin m) elemIndicesBy p e = findIndices $ p e +||| Find the indices of all elements uquals to the given one+|||+||| ```idris example+||| elemIndices 3 [1,2,3,4,3]+||| ``` elemIndices : Eq elem => elem -> Vect m elem -> List (Fin m) elemIndices = elemIndicesBy (==) @@ -418,6 +621,10 @@ --------------------------------------------------------------------------------  ||| Find all elements of a vector that satisfy some test+|||+||| ```idris example+||| filter (< 3) (fromList [1,2,3,4])+||| ``` filter : (elem -> Bool) -> Vect len elem -> (p ** Vect p elem) filter p []      = ( _ ** [] ) filter p (x::xs) =@@ -428,6 +635,10 @@         (_ ** tail)  ||| Make the elements of some vector unique by some test+|||+||| ```idris example+||| nubBy (==) (fromList [1,2,2,3,4,4])+||| ``` nubBy : (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem) nubBy = nubBy' []   where@@ -439,15 +650,29 @@         | (_ ** tail) = (_ ** x::tail)  ||| Make the elements of some vector unique by the default Boolean equality+|||+||| ```idris example+||| nub (fromList [1,2,2,3,4,4])+||| ``` nub : Eq elem => Vect len elem -> (p ** Vect p elem) nub = nubBy (==) +||| Delete first element from list according to some test+|||+||| ```idris example+||| deleteBy (<) 3 (fromList [1,2,2,3,4,4])+||| ``` deleteBy : (elem -> elem -> Bool) -> elem -> Vect len elem -> (p ** Vect p elem) deleteBy _  _ []      = (_ ** []) deleteBy eq x (y::ys) =   let (len ** zs) = deleteBy eq x ys   in if x `eq` y then (_ ** ys) else (S len ** y ::zs) +||| Delete first element from list equal to the given one+|||+||| ```idris example+||| delete 2 (fromList [1,2,2,3,4,4])+||| ``` delete : (Eq elem) => elem -> Vect len elem -> (p ** Vect p elem) delete = deleteBy (==) @@ -462,11 +687,21 @@ ||| ||| @ n   the index to split at ||| @ xs  the `Vect` to split in two+|||+||| ```idris example+||| splitAt 2 (fromList [1,2,3,4])+||| ``` splitAt : (n : Nat) -> (xs : Vect (n + m) elem) -> (Vect n elem, Vect m elem) splitAt Z xs = ([], xs) splitAt (S k) (x :: xs) with (splitAt k xs)   | (tk, dr) = (x :: tk, dr) +||| A tuple where the first element is a `Vect` of the `n` elements passing given test+||| and the second element is a `Vect` of the remaining elements of the original.+|||+||| ```idris example+||| partition (== 2) (fromList [1,2,3,2,4])+||| ``` partition : (elem -> Bool) -> Vect len elem -> ((p ** Vect p elem), (q ** Vect q elem)) partition p []      = ((_ ** []), (_ ** [])) partition p (x::xs) =@@ -480,17 +715,37 @@ -- Predicates -------------------------------------------------------------------------------- +||| Verify vector prefix+|||+||| ```idris example+||| isPrefixOfBy (==) (fromList [1,2]) (fromList [1,2,3,4])+||| ``` isPrefixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool isPrefixOfBy p [] right        = True isPrefixOfBy p left []         = False isPrefixOfBy p (x::xs) (y::ys) = p x y && isPrefixOfBy p xs ys +||| Verify vector prefix+|||+||| ```idris example+||| isPrefixOf (fromList [1,2]) (fromList [1,2,3,4])+||| ``` isPrefixOf : Eq elem => Vect m elem -> Vect len elem -> Bool isPrefixOf = isPrefixOfBy (==) +||| Verify vector suffix+|||+||| ```idris example+||| isSuffixOfBy (==) (fromList [3,4]) (fromList [1,2,3,4])+||| ``` isSuffixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right) +||| Verify vector suffix+|||+||| ```idris example+||| isSuffixOf (fromList [3,4]) (fromList [1,2,3,4])+||| ``` isSuffixOf : Eq elem => Vect m elem -> Vect len elem -> Bool isSuffixOf = isSuffixOfBy (==) @@ -498,10 +753,20 @@ -- Conversions -------------------------------------------------------------------------------- +||| Convert Maybe type into Vect+|||+||| ```idris example+||| maybeToVect (Just 2)+||| ``` maybeToVect : Maybe elem -> (p ** Vect p elem) maybeToVect Nothing  = (_ ** []) maybeToVect (Just j) = (_ ** [j]) +||| Convert first element of Vect (if exists) into Maybe.+|||+||| ```idris example+||| vectToMaybe [2]+||| ``` vectToMaybe : Vect len elem -> Maybe elem vectToMaybe []      = Nothing vectToMaybe (x::xs) = Just x@@ -510,6 +775,11 @@ -- Misc -------------------------------------------------------------------------------- +||| Filter out Nothings from Vect+|||+||| ```idris example+||| catMaybes [Just 1, Just 2, Nothing, Nothing, Just 5]+||| ``` catMaybes : Vect n (Maybe elem) -> (p ** Vect p elem) catMaybes []             = (_ ** []) catMaybes (Nothing::xs)  = catMaybes xs@@ -517,6 +787,11 @@   let (_ ** tail) = catMaybes xs    in (_ ** j::tail) +||| Get diagonal elements+|||+||| ```idris example+||| diag [[1,2,3], [4,5,6], [7,8,9]]+||| ``` diag : Vect len (Vect len elem) -> Vect len elem diag []             = [] diag ((x::xs)::xss) = x :: diag (map tail xss)@@ -530,6 +805,10 @@ ||| This is like zipping all the inner `Vect`s together and is equivalent to `traverse id` (`transposeTraverse`). ||| ||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.+|||+||| ```idris example+||| transpose [[1,2], [3,4], [5,6], [7,8]]+||| ``` transpose : Vect m (Vect n elem) -> Vect n (Vect m elem) transpose []        = replicate _ []                -- = [| [] |] transpose (x :: xs) = zipWith (::) x (transpose xs) -- = [| x :: xs |]

@@ -93,6 +93,19 @@ time = do MkRaw t <- foreign FFI_C "idris_time" (IO (Raw Integer))           pure t +||| Wall clock time+record Clock where+  constructor MkClock+  seconds : Integer+  nanoseconds : Integer++||| Get the system's wall clock time.+clockTime : IO Clock+clockTime+    = do vm <- getMyVM+         MkRaw c <- foreign FFI_C "idris_clock" (Ptr -> IO (Raw Clock)) vm+         pure c+ ||| Specify interval to sleep for in microseconds, must be nonnegative usleep : (i : Int) -> { auto prf : So (i >= 0) } -> IO () usleep i = foreign FFI_C "idris_usleep" (Int -> IO ()) i

@@ -25,6 +25,9 @@ implementation Ord a => JoinSemilattice (MaxiphobicHeap a) where   join = merge +JoinSemilattice Bool where+  join a b = a || b+ ||| Sets equipped with a binary operation that is commutative, associative and ||| idempotent.  Must satisfy the following laws: |||@@ -42,6 +45,9 @@ implementation MeetSemilattice Nat where   meet = minimum +MeetSemilattice Bool where+  meet a b = a && b+ ||| Sets equipped with a binary operation that is commutative, associative and ||| idempotent and supplied with a unitary element.  Must satisfy the following ||| laws:@@ -63,6 +69,9 @@ implementation BoundedJoinSemilattice Nat where   bottom = Z +BoundedJoinSemilattice Bool where+  bottom = False+ ||| Sets equipped with a binary operation that is commutative, associative and ||| idempotent and supplied with a unitary element.  Must satisfy the following ||| laws:@@ -81,6 +90,9 @@ interface MeetSemilattice a => BoundedMeetSemilattice a where   top : a +BoundedMeetSemilattice Bool where+  top = True+ ||| Sets equipped with two binary operations that are both commutative, ||| associative and idempotent, along with absorbtion laws for relating the two ||| binary operations.  Must satisfy the following:@@ -101,6 +113,8 @@  implementation Lattice Nat where { } +Lattice Bool where { }+ ||| Sets equipped with two binary operations that are both commutative, ||| associative and idempotent and supplied with neutral elements, along with ||| absorbtion laws for relating the two binary operations.  Must satisfy the@@ -122,3 +136,5 @@ |||     forall a,     meet a top        == top |||     forall a,     join a bottom     == bottom interface (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a where { }++BoundedLattice Bool where { }

@@ -0,0 +1,105 @@+module Control.Algebra.Laws++import Prelude.Algebra as A+import Control.Algebra+import Interfaces.Verified++%access export++||| A prof that -0 = 0 in any verified group.+inverseNeutralIsNeutral : VerifiedGroup t => inverse (the t A.neutral) = A.neutral+inverseNeutralIsNeutral {t} =+    let zero = the t neutral+        step1 = cong {f = (<+> inverse zero)} (the (zero = zero) Refl)+        step2 = replace {P = \x => zero <+> inverse zero = x} (groupInverseIsInverseL zero) step1+    in+    replace {P = \x => x = neutral} (monoidNeutralIsNeutralR $ inverse zero) step2++||| A proof that -(-x) = x in any verified group.+inverseSquaredIsIdentity : VerifiedGroup t => (x : t) -> inverse (inverse x) = x+inverseSquaredIsIdentity {t} x =+    let zero = the t neutral+        step1 = cong {f = (x <+>)} (groupInverseIsInverseL (inverse x))+        step2 = replace {P = \r => r = x <+> neutral} (semigroupOpIsAssociative x (inverse x) (inverse $ inverse x)) step1+        step3 = replace {P = \r => r <+> inverse (inverse x) = x <+> neutral} (groupInverseIsInverseL x) step2+        step4 = replace {P = \r => r = x <+> neutral} (monoidNeutralIsNeutralR (inverse $ inverse x)) step3+    in+    replace {P = \r => inverse (inverse x) = r} (monoidNeutralIsNeutralL x) step4++||| A proof that -(x + y) = -x - y in any verified abelian group.+inverseDistributesOverGroupOp : VerifiedAbelianGroup t => (l, r : t) -> inverse (l <+> r) = inverse l <+> inverse r+inverseDistributesOverGroupOp {t} l r =+    let step1 = replace {P = \x => x = neutral} (sym $ groupInverseIsInverseL (l <+> r)) $ the (the t neutral = neutral) Refl+        step2 = cong {f = ((inverse r) <+>) . ((inverse l) <+>)} step1+        step3 = replace {P = \x => inverse r <+> (inverse l <+> (l <+> r <+> inverse (l <+> r))) = inverse r <+> x} (monoidNeutralIsNeutralL (inverse l)) step2+        step4 = replace {P = \x => x = inverse r <+> inverse l} (semigroupOpIsAssociative (inverse r) (inverse l) (l <+> r <+> inverse (l <+> r))) step3+        step5 = replace {P = \x => x = inverse r <+> inverse l} (semigroupOpIsAssociative (inverse r <+> inverse l) (l <+> r) (inverse (l <+> r))) step4+        step6 = replace {P = \x => x <+> inverse (l <+> r) = inverse r <+> inverse l} (semigroupOpIsAssociative (inverse r <+> inverse l) l r) step5+        step7 = replace {P = \x => x <+> r <+> inverse (l <+> r) = inverse r <+> inverse l} (sym $ semigroupOpIsAssociative (inverse r) (inverse l) l) step6+        step8 = replace {P = \x => inverse r <+> x <+> r <+> inverse (l <+> r) = inverse r <+> inverse l} (groupInverseIsInverseR l) step7+        step9 = replace {P = \x => x <+> r <+> inverse (l <+> r) = inverse r <+> inverse l} (monoidNeutralIsNeutralL (inverse r)) step8+        step10 = replace {P = \x => x <+> inverse (l <+> r) = inverse r <+> inverse l} (groupInverseIsInverseR r) step9+        step11 = replace {P = \x => x = inverse r <+> inverse l} (monoidNeutralIsNeutralR (inverse (l <+> r))) step10+    in+    replace {P = \x => inverse (l <+> r) = x} (abelianGroupOpIsCommutative (inverse r) (inverse l)) step11++||| A proof that anything multiplied by zero yields zero back.+multNeutralAbsorbingL : VerifiedRingWithUnity t => (r : t) -> A.neutral <.> r = A.neutral+multNeutralAbsorbingL r =+    let step1 = the (unity <.> r = r) (ringWithUnityIsUnityR r)+        step2 = replace {P = \x => x <.> r = r} (sym $ monoidNeutralIsNeutralR unity) step1+        step3 = replace {P = \x => x = r} (ringOpIsDistributiveR neutral unity r) step2+        step4 = replace {P = \x => neutral <.> r <+> x = r} (ringWithUnityIsUnityR r) step3+        step5 = cong {f = \x => x <+> inverse r} step4+        step6 = replace {P = \x => x = r <+> inverse r} (sym $ semigroupOpIsAssociative (neutral <.> r) r (inverse r)) step5+        step7 = replace {P = \x => neutral <.> r <+> x = x} (groupInverseIsInverseL r) step6+    in+    replace {P = \x => x = neutral} (monoidNeutralIsNeutralL (neutral <.> r)) step7++||| A proof that anything multiplied by zero yields zero back.+multNeutralAbsorbingR : VerifiedRingWithUnity t => (l : t) -> l <.> A.neutral = A.neutral+multNeutralAbsorbingR l =+    let step1 = the (l <.> unity = l) (ringWithUnityIsUnityL l)+        step2 = replace {P = \x => l <.> x = l} (sym $ monoidNeutralIsNeutralR unity) step1+        step3 = replace {P = \x => x = l} (ringOpIsDistributiveL l neutral unity) step2+        step4 = replace {P = \x => l <.> neutral <+> x = l} (ringWithUnityIsUnityL l) step3+        step5 = cong {f = \x => x <+> inverse l} step4+        step6 = replace {P = \x => x = l <+> inverse l} (sym $ semigroupOpIsAssociative (l <.> neutral) l (inverse l)) step5+        step7 = replace {P = \x => l <.> neutral <+> x = x} (groupInverseIsInverseL l) step6+    in+    replace {P = \x => x = neutral} (monoidNeutralIsNeutralL (l <.> neutral)) step7++||| A proof that inverse operator can be extracted before multiplication+||| (-x)y = -(xy)+multInverseInversesL : VerifiedRingWithUnity t => (l, r : t) -> inverse l <.> r = inverse (l <.> r)+multInverseInversesL l r =+    let step1 = replace {P = \x => x <.> r = neutral} (sym $ groupInverseIsInverseL l) (multNeutralAbsorbingL r)+        step2 = replace {P = \x => x = neutral} (ringOpIsDistributiveR l (inverse l) r) step1+        step3 = cong {f = ((inverse (l <.> r)) <+>)} step2+        step4 = replace {P = \x => inverse (l <.> r) <+> (l <.> r <+> inverse l <.> r) = x} (monoidNeutralIsNeutralL (inverse (l <.> r))) step3+        step5 = replace {P = \x => x = inverse (l <.> r)} (semigroupOpIsAssociative (inverse (l <.> r)) (l <.> r) (inverse l <.> r)) step4+        step6 = replace {P = \x => x <+> inverse l <.> r = inverse (l <.> r)} (groupInverseIsInverseR (l <.> r)) step5+    in+    replace {P = \x => x = inverse (l <.> r)} (monoidNeutralIsNeutralR (inverse l <.> r)) step6++||| A proof that inverse operator can be extracted before multiplication+||| x(-y) = -(xy)+multInverseInversesR : VerifiedRingWithUnity t => (l, r : t) -> l <.> inverse r = inverse (l <.> r)+multInverseInversesR l r =+    let step1 = replace {P = \x => l <.> x = neutral} (sym $ groupInverseIsInverseL r) (multNeutralAbsorbingR l)+        step2 = replace {P = \x => x = neutral} (ringOpIsDistributiveL l r (inverse r)) step1+        step3 = cong {f = ((inverse (l <.> r)) <+>)} step2+        step4 = replace {P = \x => inverse (l <.> r) <+> (l <.> r <+> l <.> inverse r) = x} (monoidNeutralIsNeutralL (inverse (l <.> r))) step3+        step5 = replace {P = \x => x = inverse (l <.> r)} (semigroupOpIsAssociative (inverse (l <.> r)) (l <.> r) (l <.> inverse r)) step4+        step6 = replace {P = \x => x <+> l <.> inverse r = inverse (l <.> r)} (groupInverseIsInverseR (l <.> r)) step5+    in+    replace {P = \x => x = inverse (l <.> r)} (monoidNeutralIsNeutralR (l <.> inverse r)) step6++||| A proof that multiplication of inverses is the same as multiplication of original+||| elements. (-x)(-y) = xy+multNegativeByNegativeIsPositive : VerifiedRingWithUnity t => (l, r : t) -> inverse l <.> inverse r = l <.> r+multNegativeByNegativeIsPositive l r =+    rewrite multInverseInversesR (inverse l) r in+    rewrite sym $ multInverseInversesL (inverse l) r in+    rewrite inverseSquaredIsIdentity l in+    Refl

@@ -3,6 +3,12 @@ %access public export %default total +notInvolutive : (x : Bool) -> not (not x) = x+notInvolutive True  = Refl+notInvolutive False = Refl++-- AND+ andSameNeutral : (x : Bool) -> x && x = x andSameNeutral False = Refl andSameNeutral True = Refl@@ -15,6 +21,20 @@ andTrueNeutral False = Refl andTrueNeutral True = Refl +andAssociative : (x, y, z : Bool) -> x && (y && z) = (x && y) && z+andAssociative True  _ _ = Refl+andAssociative False _ _ = Refl++andCommutative : (x, y : Bool) -> x && y = y && x+andCommutative x True  = andTrueNeutral x+andCommutative x False = andFalseFalse x++andNotFalse : (x : Bool) -> x && not x = False+andNotFalse False = Refl+andNotFalse True = Refl++-- OR+ orSameNeutral : (x : Bool) -> x || x = x orSameNeutral False = Refl orSameNeutral True = Refl@@ -27,6 +47,36 @@ orTrueTrue False = Refl orTrueTrue True = Refl -orSameAndRightNeutral : (x, right : Bool) -> x || (x && right) = x+orAssociative : (x, y, z : Bool) -> x || (y || z) = (x || y) || z+orAssociative True  _ _ = Refl+orAssociative False _ _ = Refl++orCommutative : (x, y : Bool) -> x || y = y || x+orCommutative x True  = orTrueTrue x+orCommutative x False = orFalseNeutral x++orNotTrue : (x : Bool) -> x || not x = True+orNotTrue False = Refl+orNotTrue True = Refl++-- interaction & De Morgan's laws++orSameAndRightNeutral : (x, y : Bool) -> x || (x && y) = x orSameAndRightNeutral False _ = Refl-orSameAndRightNeutral True _ = Refl+orSameAndRightNeutral True  _ = Refl++andDistribOrR : (x, y, z : Bool) -> x && (y || z) = (x && y) || (x && z)+andDistribOrR False _ _ = Refl+andDistribOrR True  _ _ = Refl++orDistribAndR : (x, y, z : Bool) -> x || (y && z) = (x || y) && (x || z)+orDistribAndR False _ _ = Refl+orDistribAndR True  _ _ = Refl++notAndIsOr : (x, y : Bool) -> not (x && y) = not x || not y+notAndIsOr False _ = Refl+notAndIsOr True  _ = Refl++notOrIsAnd : (x, y : Bool) -> not (x || y) = not x && not y+notOrIsAnd False _ = Refl+notOrIsAnd True  _ = Refl

@@ -2,8 +2,85 @@  import Data.Fin +%access public export+%default total++ ||| Proof that an element **n** of Fin **m** , when converted to Nat is smaller than the bound **m**.-public export elemSmallerThanBound : (n : Fin m) -> LT (finToNat n) m elemSmallerThanBound FZ = LTESucc LTEZero elemSmallerThanBound (FS x) = LTESucc (elemSmallerThanBound x)++||| Proof that application of finToNat the last element of Fin **S n** gives **n**.+finToNatLastIsBound : finToNat (Fin.last {n}) = n+finToNatLastIsBound {n=Z} = Refl+finToNatLastIsBound {n=S k} = rewrite finToNatLastIsBound {n=k} in Refl++||| Proof that an element **n** of Fin **m** , when converted to Nat is smaller than the bound **m**.+finToNatWeakenNeutral : {n : Fin m} -> finToNat (weaken n) = finToNat n+finToNatWeakenNeutral {n=FZ} = Refl+finToNatWeakenNeutral {m=S (S _)} {n=FS _} = cong finToNatWeakenNeutral++||| Proof that it's possible to strengthen a weakened element of Fin **m**.+strengthenWeakenNeutral : (n : Fin m) -> strengthen (weaken n) = Right n+strengthenWeakenNeutral {m=S _} FZ = Refl+strengthenWeakenNeutral {m=S (S _)} (FS k) = rewrite strengthenWeakenNeutral k in Refl++||| Proof that it's not possible to strengthen the last element of Fin **n**.+strengthenLastIsLeft : strengthen (Fin.last {n}) = Left (Fin.last {n})+strengthenLastIsLeft {n=Z} = Refl+strengthenLastIsLeft {n=S k} = rewrite strengthenLastIsLeft {n=k} in Refl++||| Enumerate elements of Fin **n** backwards.+invFin : Fin n -> Fin n+invFin FZ = last+invFin {n=S (S _)} (FS k) = weaken (invFin k)++||| Proof that an inverse of a weakened element of Fin **n** is a successive of an inverse of an original element.+invWeakenIsSucc : (m : Fin n) -> invFin (weaken m) = FS (invFin m)+invWeakenIsSucc FZ = Refl+invWeakenIsSucc {n=S (S _)} (FS k) = rewrite invWeakenIsSucc k in Refl++||| Proof that double inversion of Fin **n** gives the original.+doubleInvFinSame : (m : Fin n) -> invFin (invFin m) = m+doubleInvFinSame {n=S Z} FZ = Refl+doubleInvFinSame {n=S (S k)} FZ = rewrite doubleInvFinSame {n=S k} FZ in Refl+doubleInvFinSame {n=S (S _)} (FS x) = trans (invWeakenIsSucc $ invFin x) (cong $ doubleInvFinSame x)++||| Proof that an inverse of the last element of Fin (S **n**) in FZ.+invLastIsFZ : invFin (Fin.last {n}) = FZ+invLastIsFZ {n=Z} = Refl+invLastIsFZ {n=S k} = rewrite invLastIsFZ {n=k} in Refl++||| Proof that it's possible to strengthen an inverse of a succesive element of Fin **n**.+strengthenNotLastIsRight : (m : Fin (S n)) -> strengthen (invFin (FS m)) = Right (invFin m)+strengthenNotLastIsRight m = strengthenWeakenNeutral (invFin m)++||| Either tightens the bound on a Fin or proves that it's the last.+strengthen' : (m : Fin (S n)) -> Either (m = Fin.last) (m' : Fin n ** finToNat m = finToNat m')+strengthen' {n = Z} FZ = Left Refl+strengthen' {n = S k} FZ = Right (FZ ** Refl)+strengthen' {n = S k} (FS m) with (strengthen' m)+    | Left eq   = Left $ cong eq+    | Right (m' ** eq)  = Right (FS m' ** cong eq)++||| A view of Nat as a quotient of some number and a finite remainder.+data FractionView : (n : Nat) -> (d : Nat) -> Type where+    Fraction : (n : Nat) -> (d : Nat) -> {auto ok: GT d Z} ->+                (q : Nat) -> (r : Fin d) ->+                q * d + finToNat r = n -> FractionView n d++||| Converts Nat to the fractional view with a non-zero divisor.+divMod : (n, d : Nat) -> {auto ok: GT d Z} -> FractionView n d+divMod Z (S d) = Fraction Z (S d) Z FZ Refl+divMod (S n) (S d) with (divMod n (S d))+    | (Fraction n (S d) q r eq) with (strengthen' r)+        | Left eq' = Fraction (S n) (S d) (S q) FZ $+            rewrite sym eq in+                rewrite trans (cong {f=finToNat} eq') finToNatLastIsBound in+                    cong $ trans+                        (plusZeroRightNeutral (d + q * S d))+                        (plusCommutative d (q * S d))+        | Right (r' ** eq') = Fraction (S n) (S d) q (FS r') $+            rewrite sym $ plusSuccRightSucc (q * S d) (finToNat r') in+                cong $ trans (sym $ cong {f=plus (q * S d)} eq') eq

@@ -3,13 +3,15 @@ %default total %access export +||| The final segment of the accumulator is the final segment of the result.+reverseOntoAcc : (xs, ys, zs : List a) ->+  reverseOnto (ys ++ zs) xs = (reverseOnto ys xs) ++ zs+reverseOntoAcc [] _ _ = Refl+reverseOntoAcc (x :: xs) (ys) (zs) = reverseOntoAcc xs (x :: ys) zs+ ||| Serves as a specification for reverseOnto. reverseOntoSpec : (xs, ys : List a) -> reverseOnto xs ys = reverse ys ++ xs-reverseOntoSpec _  [] = Refl-reverseOntoSpec xs (y::ys) =-  trans (reverseOntoSpec (y::xs) ys)-        (trans (appendAssociative (reverse ys) [y] xs)-               (cong {f = \l => l ++ xs} (sym (reverseOntoSpec [y] ys))))+reverseOntoSpec xs ys = reverseOntoAcc ys [] xs  ||| The reverse of an empty list is an empty list.  Together with reverseCons, ||| serves as a specification for reverse.@@ -26,10 +28,10 @@   reverse (xs ++ ys) = reverse ys ++ reverse xs reverseAppend [] ys = sym (appendNilRightNeutral (reverse ys)) reverseAppend (x :: xs) ys =-  trans (trans (reverseCons x (xs ++ ys))-               (cong {f = \l => l ++ [x]} (reverseAppend xs ys)))-        (sym (trans (cong (reverseCons x xs))-                    (appendAssociative (reverse ys) (reverse xs) [x])))+  rewrite reverseCons x (xs ++ ys) in+    rewrite reverseAppend xs ys in+      rewrite reverseCons x xs in+        sym $ appendAssociative (reverse ys) (reverse xs) [x]  ||| Reversing a singleton list is a no-op. reverseSingletonId : (x : a) -> reverse [x] = [x]@@ -39,6 +41,6 @@ reverseReverseId : (xs : List a) -> reverse (reverse xs) = xs reverseReverseId [] = Refl reverseReverseId (x :: xs) =-  trans (cong (reverseCons x xs))-        (trans (reverseAppend (reverse xs) [x])-               (cong (reverseReverseId xs)))+  rewrite reverseCons x xs in+    rewrite reverseAppend (reverse xs) [x] in+      cong $ reverseReverseId xs

@@ -0,0 +1,161 @@+module Data.Logic.Propositional++%default total+%access public export++-- Idris uses intuitionistic logic, so it does not validate the+-- principle of excluded middle (PEM) or similar theorems of classical+-- logic. But it does validate certain relations among these+-- propositions, and that's what's in this file.++||| The principle of excluded middle+PEM : Type -> Type+PEM p = Either p (Not p)++||| Double negation elimination+DNE : Type -> Type+DNE p = Not $ Not p -> p++||| The consensus theorem (at least, the interesting part)+Consensus : Type -> Type -> Type -> Type+Consensus p q r = (q, r) -> Either (p, q) (Not p, r)++||| Peirce's law+Peirce : Type -> Type -> Type+Peirce p q = ((p -> q) -> p) -> p++||| Not sure if this one has a name, so call it Frege's law+Frege : Type -> Type -> Type -> Type+Frege p q r = (p -> r) -> (q -> r) -> ((p -> q) -> q) -> r++||| The converse of contraposition: (p -> q) -> Not q -> Not p+Transposition : Type -> Type -> Type+Transposition p q = (Not q -> Not p) -> p -> q++||| This isn't a good name.+Switch : Type -> Type+Switch p = (Not p -> p) -> p++-- PEM and the others can't be proved outright, but it is possible to+-- prove the double negations (DN) of all of them.++||| The double negation of a proposition+DN : Type -> Type+DN p = Not $ Not p++pemDN : DN $ PEM p+pemDN f = f $ Right $ \x => f $ Left x++dneDN : DN $ DNE p+dneDN f = f $ \g => void $ g $ \x => f $ \_ => x++consensusDN : DN $ Consensus p q r+consensusDN f = f $ \(y, z) => Right (\x => f $ \(_, _) => Left (x, y), z)++peirceDN : DN $ Peirce p q+peirceDN f = f $ \g => g $ \x => void $ f $ \_ => x++fregeDN : DN $ Frege p q r+fregeDN f = f $ \g, h, i => h $ i $ \x => void $ f $ \_, _, _ => g x++transpositionDN : DN $ Transposition p q+transpositionDN f = f $ \g, x => void $ g (\y => f $ \_, _ => y) x++switchDN : DN $ Switch p+switchDN f = f $ \g => g $ \x => f $ \_ => x++-- It's easy to prove all these theorems assuming PEM.++dnePEM : PEM p -> DNE p+dnePEM (Left l) _ = l+dnePEM (Right r) f = void $ f r++consensusPEM : PEM p -> Consensus p q r+consensusPEM (Left l) (y, _) = Left (l, y)+consensusPEM (Right r) (_, z) = Right (r, z)++peircePEM : PEM p -> Peirce p q+peircePEM (Left l) _ = l+peircePEM (Right r) f = f $ \x => void $ r x++fregePEM : PEM p -> Frege p q r+fregePEM (Left l) f _ _ = f l+fregePEM (Right r) _ g h = g $ h $ \x => void $ r x++transpositionPEM : PEM p -> Transposition q p+transpositionPEM (Left l) _ _ = l+transpositionPEM (Right r) f x = void $ f r x++switchPEM : PEM p -> Switch p+switchPEM (Left l) _ = l+switchPEM (Right r) f = f r++-- It's trivial to prove these theorems assuming double negation+-- elimination (DNE), since their double negations can all be proved.++||| Eliminate double negations+EDN : DN p -> DNE p -> p+EDN f g = g f++pemDNE : DNE $ PEM p -> PEM p+pemDNE = EDN pemDN++-- It's possible to prove the theorems assuming Peirce's law, but some+-- thought must be given to choosing the right instances. Peirce's law+-- is therefore weaker than PEM on an instance-by-instance basis, but+-- all the instances together are equivalent.++pemPeirce : Peirce (PEM p) Void -> PEM p+pemPeirce f = f $ \g => Right $ \x => g $ Left x++dnePeirce : Peirce p Void -> DNE p+dnePeirce f g = f $ \h => void $ g h++consensusPeirce : Peirce (Consensus p q r) Void -> Consensus p q r+consensusPeirce f (y, z) =+  f (\g, (_, _) => Right (\x => g (\_ => Left (x, y)), z)) (y, z)++fregePeirce : Peirce (Frege p q r) Void -> Frege p q r+fregePeirce f g h i =+  f (\j, _, _, _ => h $ i $ \x => void $ j $ \_, _, _ => g x) g h i++transpositionPeirce : Peirce (Transposition p q) Void -> Transposition p q+transpositionPeirce f g x =+  f (\h, _, _ => void $ g (\y => h $ \_, _ => y) x) (\j, _ => g j x) x++-- There are a variety of single axioms sufficient for deriving all of+-- classical logic. The earliest of these is known as Nicod's axiom,+-- but it is written using only nand operators and doesn't lend itself+-- to Idris's type system. Meredith's axiom, on the other hand, is+-- written using implication and negation.++||| Meredith's axiom, sufficient for deriving all of classical logic+Meredith : (p, q, r, s, t : Type) -> Type+Meredith p q r s t =+  ((((p -> q) -> Not r -> Not s) -> r) -> t) -> (t -> p) -> s -> p++-- The Meredith axiom implies all of classical logic, and so in+-- particular it implies PEM, and therefore cannot be proved in+-- intuitionistic logic. As usual, however, its double negation can be+-- proved.++meredithDN : DN $ Meredith p q r s t+meredithDN f =+  f $ \g, h, x =>+    h $ g $ \i =>+      void $ i+        (\y => void $ f $ \_, _, _ => y)+        (\z => f $ \_, _, _ => h $ g $ \_ => z)+        x++-- Meredith can be proved assuming PEM, since the type system itself+-- takes care of the rest.++meredithPEM : PEM p -> Meredith p q r s t+meredithPEM (Left l) _ _ _ = l+meredithPEM (Right r) f g x =+  g $ f $ \h =>+    void $ h+      (\y => void $ r y)+      (\z => r $ g $ f (\_ => z))+      x

@@ -1,8 +1,25 @@ module Data.Nat  %default total+%access public export  diff : Nat -> Nat -> Nat diff k Z = k diff Z j = j diff (S k) (S j) = diff k j++ltePlus : LTE m1 n1 -> LTE m2 n2 -> LTE (m1 + m2) (n1 + n2)+ltePlus {n1=Z} LTEZero lte = lte+ltePlus {n1=S k} LTEZero lte = lteSuccRight $ ltePlus {n1=k} LTEZero lte+ltePlus (LTESucc lte1) lte2 = LTESucc $ ltePlus lte1 lte2++lteCongPlus : (k : Nat) -> LTE m n -> LTE (m + k) (n + k)+lteCongPlus k lte = ltePlus lte lteRefl++lteMult : LTE m1 n1 -> LTE m2 n2 -> LTE (m1 * m2) (n1 * n2)+lteMult LTEZero _ = LTEZero+lteMult {m1=S k} (LTESucc _) LTEZero = rewrite multZeroRightZero k in LTEZero+lteMult (LTESucc lte1) (LTESucc lte2) = LTESucc $ ltePlus lte2 $ lteMult lte1 $ LTESucc lte2++lteCongMult : (k : Nat) -> LTE m n -> LTE (m * k) (n * k)+lteCongMult k lte = lteMult lte lteRefl

@@ -0,0 +1,50 @@+||| Properties of the Fibonacci function.+module Data.Nat.Fib++%access public export++%default total++||| Recursive definition of Fibonacci.+fibRec : Nat -> Nat+fibRec Z = Z+fibRec (S Z) = S Z+fibRec (S (S k)) = fibRec (S k) + fibRec k++||| Accumulator for fibItr.+fibAcc : Nat -> Nat -> Nat -> Nat+fibAcc Z a _ = a+fibAcc (S k) a b = fibAcc k b (a + b)++||| Iterative definition of Fibonacci.+fibItr : Nat -> Nat+fibItr n = fibAcc n 0 1++||| Addend shuffling lemma.+plusLemma : (a, b, c, d : Nat) -> (a + b) + (c + d) = (a + c) + (b + d)+plusLemma a b c d =+  rewrite sym $ plusAssociative a b (c + d) in+    rewrite plusAssociative b c d in+      rewrite plusCommutative b c in+        rewrite sym $ plusAssociative c b d in+          plusAssociative a c (b + d)++||| Helper lemma for fibacc.+fibAdd : (n, a, b, c, d : Nat) ->+  fibAcc n a b + fibAcc n c d = fibAcc n (a + c) (b + d)+fibAdd Z _ _ _ _ = Refl+fibAdd (S Z) _ _ _ _ = Refl+fibAdd (S (S k)) a b c d =+  rewrite fibAdd k (a + b) (b + (a + b)) (c + d) (d + (c + d)) in+    rewrite plusLemma b (a + b) d (c + d) in+      rewrite plusLemma a b c d in+        Refl++||| Iterative and recursive Fibonacci definitions are equivalent.+fibEq : (n : Nat) -> fibRec n = fibItr n+fibEq Z = Refl+fibEq (S Z) = Refl+fibEq (S (S k)) =+  rewrite fibEq k in+    rewrite fibEq (S k) in+      fibAdd k 1 1 0 1

@@ -14,3 +14,78 @@   odd : Nat -> Bool   odd Z = False   odd (S k) = even k++||| A nat is Even when it is twice some other nat.+Even : Nat -> Type+Even n = (half : Nat ** n = half * 2)++||| A nat is Odd when it is one more than twice some other nat.+Odd : Nat -> Type+Odd n = (haf : Nat ** n = S $ haf * 2)++||| Two more than an Even is Even.+add2Even : Even n -> Even (2 + n)+add2Even (half ** pf) = (S half ** cong {f = (+) 2} pf)++||| Two more than an Odd is Odd.+add2Odd : Odd n -> Odd (2 + n)+add2Odd (haf ** pf) = (S haf ** cong {f = (+) 2} pf)++||| One more than an Even is Odd.+succEvenOdd : Even n -> Odd (S n)+succEvenOdd (half ** pf) = (half ** cong {f = S} pf)++||| One more than an Odd is Even.+succOddEven : Odd n -> Even (S n)+succOddEven (haf ** pf) = (S haf ** cong {f = S} pf)++||| One less than an Odd is Even.+predOddEven : Odd (S n) -> Even n+predOddEven (haf ** pf) = (haf ** cong {f = Nat.pred} pf)++||| A helper fact.+succDoublePredPred : S n = k * 2 -> n = S $ (pred k) * 2+succDoublePredPred {k = Z} prf = absurd prf+succDoublePredPred {k = S _} prf = cong {f = Nat.pred} prf++||| One less than an Even is Odd.+predEvenOdd : Even (S n) -> Odd n+predEvenOdd (half ** pf) = (pred half ** succDoublePredPred pf)++||| Every nat is either Even or Odd.+evenOrOdd : (n : Nat) -> Either (Even n) (Odd n)+evenOrOdd Z = Left (0 ** Refl)+evenOrOdd (S k) = case evenOrOdd k of+  Left (half ** pf) => Right (half ** cong {f = S} pf)+  Right (haf ** pf) => Left (S haf ** cong {f = S} pf)++||| No nat is both Even and Odd.+notEvenAndOdd : Even n -> Odd n -> Void+notEvenAndOdd {n = Z} _ (_ ** odd) = absurd odd+notEvenAndOdd {n = (S k)} (half ** even) (haf ** odd) =+  notEvenAndOdd {n = k}+   (haf ** cong {f = Nat.pred} odd)+   (pred half ** succDoublePredPred even)++||| Evenness is decidable.+evenDec : (n : Nat) -> Dec $ Even n+evenDec n = case evenOrOdd n of+  Left even => Yes even+  Right odd => No $ \even => notEvenAndOdd even odd++||| Oddness is decidable.+oddDec : (n : Nat) -> Dec $ Odd n+oddDec n = case evenOrOdd n of+  Left even => No $ notEvenAndOdd even+  Right odd => Yes odd++mutual+  ||| Evens are even.+  evenEven : Even n -> even n = True+  evenEven {n = Z} _ = Refl+  evenEven {n = S _} pf = oddOdd $ predEvenOdd pf++  ||| Odds are odd.+  oddOdd : Odd n -> odd n = True+  oddOdd {n = Z} (_ ** pf) = absurd pf+  oddOdd {n = S _} pf = evenEven $ predOddEven pf

@@ -287,6 +287,10 @@ mergeLeft : SortedMap k v -> SortedMap k v -> SortedMap k v mergeLeft = mergeWith const +export+(Show k, Show v) => Show (SortedMap k v) where+   show m = "fromList " ++ (show $ toList m)+ -- TODO: is this the right variant of merge to use for this? I think it is, but -- I could also see the advantages of using `mergeLeft`. The current approach is -- strictly more powerful I believe, because `mergeLeft` can be emulated with

@@ -0,0 +1,32 @@+module Interfaces.Proposition++%default total+%access public export+++||| A canonical proof that some type containing no more than one value,+||| comprising a mere proposition.+interface Proposition t where+  ||| If there are two values of t, prove that they are actually the same+  atMostOneValue : (x : t) -> (y : t) -> x = y++Proposition () where+  atMostOneValue () () = Refl++Proposition Void where+  atMostOneValue _ _ impossible+  +Proposition (x = y) where+  atMostOneValue Refl Refl = Refl++Proposition (LTE m n) where+  atMostOneValue {m=Z} LTEZero LTEZero = Refl+  atMostOneValue {m=S _} (LTESucc x) (LTESucc y) = cong $ atMostOneValue x y+  +Proposition (NonEmpty xs) where+  atMostOneValue IsNonEmpty IsNonEmpty = Refl++(Proposition a, Proposition b) => Proposition (a, b) where+  atMostOneValue (x1, y1) (x2, y2) =+    rewrite atMostOneValue x1 x2 in+      rewrite atMostOneValue y1 y2 in Refl

@@ -6,6 +6,7 @@ import Control.Algebra.VectorSpace import Data.Vect import Data.ZZ+import Data.Bool.Extra  %default total %access public export@@ -317,7 +318,42 @@   joinSemilatticeJoinIsCommutative : (l, r : a)    -> join l r = join r l   joinSemilatticeJoinIsIdempotent  : (e : a)       -> join e e = e +VerifiedJoinSemilattice Nat where+  joinSemilatticeJoinIsAssociative = maximumAssociative+  joinSemilatticeJoinIsCommutative = maximumCommutative+  joinSemilatticeJoinIsIdempotent  = maximumIdempotent++VerifiedJoinSemilattice Bool where+  joinSemilatticeJoinIsAssociative = orAssociative+  joinSemilatticeJoinIsCommutative = orCommutative+  joinSemilatticeJoinIsIdempotent = orSameNeutral+ interface MeetSemilattice a => VerifiedMeetSemilattice a where   meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r   meetSemilatticeMeetIsCommutative : (l, r : a)    -> meet l r = meet r l   meetSemilatticeMeetIsIdempotent  : (e : a)       -> meet e e = e++VerifiedMeetSemilattice Nat where+  meetSemilatticeMeetIsAssociative = minimumAssociative+  meetSemilatticeMeetIsCommutative = minimumCommutative+  meetSemilatticeMeetIsIdempotent  = minimumIdempotent++VerifiedMeetSemilattice Bool where+  meetSemilatticeMeetIsAssociative = andAssociative+  meetSemilatticeMeetIsCommutative = andCommutative+  meetSemilatticeMeetIsIdempotent = andSameNeutral++interface (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where+  joinBottomIsIdentity : (x : a) -> join x Lattice.bottom = x++VerifiedBoundedJoinSemilattice Nat where+  joinBottomIsIdentity = maximumZeroNLeft++VerifiedBoundedJoinSemilattice Bool where+  joinBottomIsIdentity = orFalseNeutral+  +interface (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where+  meetTopIsIdentity : (x : a) -> meet x Lattice.top = x++VerifiedBoundedMeetSemilattice Bool where+  meetTopIsIdentity = andTrueNeutral

@@ -30,10 +30,12 @@ getAction : CGI a -> CGIInfo -> IO (a, CGIInfo) getAction (MkCGI act) = act +export implementation Functor CGI where     map f (MkCGI c) = MkCGI (\s => do (a, i) <- c s                                       pure (f a, i)) +export implementation Applicative CGI where     pure v = MkCGI (\s => pure (v, s)) @@ -41,6 +43,7 @@                                               (c, j) <- b i                                               pure (f c, j)) +export implementation Monad CGI where     (>>=) (MkCGI f) k = MkCGI (\s => do v <- f s                                         getAction (k (fst v)) (snd v))

@@ -71,15 +71,15 @@   show AF_INET6  = "AF_INET6"  ToCode SocketFamily where-  toCode AF_UNSPEC = 0-  toCode AF_INET   = 2-  toCode AF_INET6  = 10+  toCode AF_UNSPEC = unsafePerformIO (foreign FFI_C "#AF_UNSPEC" (IO Int))+  toCode AF_INET   = unsafePerformIO (foreign FFI_C "#AF_INET" (IO Int))+  toCode AF_INET6  = unsafePerformIO (foreign FFI_C "#AF_INET6" (IO Int))  getSocketFamily : Int -> Maybe SocketFamily getSocketFamily i =-    Prelude.List.lookup i [ (0, AF_UNSPEC)-                          , (2, AF_INET)-                          , (10, AF_INET6)+    Prelude.List.lookup i [ (toCode AF_UNSPEC, AF_UNSPEC)+                          , (toCode AF_INET, AF_INET)+                          , (toCode AF_INET6, AF_INET6)                           ]  -- ------------------------------------------------------------ [ Socket Types ]

@@ -161,14 +161,14 @@ hexDigits = some hexDigit  ||| Recognise a single octal digit-||| /[0-8]/+||| /[0-7]/ octDigit : Lexer-octDigit = pred isHexDigit+octDigit = pred isOctDigit  ||| Recognise one or more octal digits-||| /[0-8]+/+||| /[0-7]+/ octDigits : Lexer-octDigits = some hexDigit+octDigits = some octDigit  ||| Recognise a single alpha character ||| /[A-Za-z]/

@@ -8,6 +8,7 @@          , Control.Algebra         , Control.Algebra.Lattice+        , Control.Algebra.Laws         , Control.Algebra.NumericImplementations         , Control.Algebra.VectorSpace @@ -70,6 +71,7 @@          , Interfaces.Correlative         , Interfaces.Verified+        , Interfaces.Proposition          , Language.JSON         , Language.JSON.Data

@@ -12,7 +12,7 @@ ||| The underlying implementation of the if ... then ... else ... syntax ||| @ b the condition on the if ||| @ t the value if b is true-||| @ e the falue if b is false+||| @ e the value if b is false ifThenElse : (b : Bool) -> (t : Lazy a) -> (e : Lazy a) -> a ifThenElse True  t e = t ifThenElse False t e = e

@@ -13,6 +13,7 @@ import Prelude.Interfaces import Prelude.Either import Prelude.Show+ import IO  %access public export@@ -108,12 +109,12 @@ data Mode = Read | WriteTruncate | Append | ReadWrite | ReadWriteTruncate | ReadAppend  modeStr : Mode -> String-modeStr Read              = "r"-modeStr WriteTruncate     = "w"-modeStr Append            = "a"-modeStr ReadWrite         = "r+"-modeStr ReadWriteTruncate = "w+"-modeStr ReadAppend        = "a+"+modeStr Read              = "rb"+modeStr WriteTruncate     = "wb"+modeStr Append            = "ab"+modeStr ReadWrite         = "rb+"+modeStr ReadWriteTruncate = "wb+"+modeStr ReadAppend        = "ab+"  ||| Open a file ||| @ f the filename@@ -287,6 +288,17 @@ fEOF : File -> IO Bool fEOF (FHandle h) = do eof <- do_feof h                       pure (not (eof == 0))++private+do_fremove : String -> IO Int+do_fremove s = foreign FFI_C "fileRemove" (String -> IO Int) s++||| Remove a file+||| @s the file name+export+fRemove : (s : String) -> IO Bool+fRemove s = do res <- do_fremove s+               pure (res == 0)  export fpoll : File -> IO Bool

@@ -113,13 +113,19 @@     compare x y = if (x == y) then EQ else                   if (boolOp prim__sltInt x y) then LT else                   GT-+    (<) x y = boolOp prim__sltInt x y+    (>) x y = boolOp prim__sgtInt x y +    (<=) x y = boolOp prim__slteInt x y+    (>=) x y = boolOp prim__sgteInt x y   Ord Integer where     compare x y = if (x == y) then EQ else                   if (boolOp prim__sltBigInt x y) then LT else                   GT-+    (<) x y = boolOp prim__sltBigInt x y+    (>) x y = boolOp prim__sgtBigInt x y +    (<=) x y = boolOp prim__slteBigInt x y+    (>=) x y = boolOp prim__sgteBigInt x y   Ord Double where     compare x y = if (x == y) then EQ else

@@ -436,12 +436,12 @@ ||| |||     transpose [[], [1, 2]] = [[1], [2]] |||     transpose (transpose [[], [1, 2]]) = [[1, 2]]-|||-||| TODO: Solution which satisfies the totality checker? transpose : List (List a) -> List (List a) transpose [] = []-transpose ([] :: xss) = transpose xss-transpose ((x::xs) :: xss) = assert_total $ (x :: (mapMaybe head' xss)) :: (transpose (xs :: (map (drop 1) xss)))+transpose (heads :: tails) = spreadHeads heads (transpose tails) where+  spreadHeads []              tails           = tails+  spreadHeads (head :: heads) []              = [head] :: spreadHeads heads []+  spreadHeads (head :: heads) (tail :: tails) = (head :: tail) :: spreadHeads heads tails  -------------------------------------------------------------------------------- -- Membership tests@@ -860,6 +860,12 @@ -------------------------------------------------------------------------------- -- Properties --------------------------------------------------------------------------------++Uninhabited ([] = _ :: _) where+  uninhabited Refl impossible++Uninhabited (_ :: _ = []) where+  uninhabited Refl impossible  ||| (::) is injective consInjective : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->

@@ -1,6 +1,6 @@ .\" Manpage for Idris. .\" Contact <> to correct errors or typos.-.TH man 1 "23 October 2018" "1.3.1" "Idris man page"+.TH man 1 "23 October 2018" "1.3.2" "Idris man page" .SH NAME idris -\ a general purpose pure functional programming language with dependent types. .SH SYNOPSIS@@ -99,6 +99,10 @@                            e.g. corei7 or cortex-m3.   --color,--colour         Force coloured output   --nocolor,--nocolour     Disable coloured output+  --optimise-nat-like-types,--optimize-nat-like-types+                           Compile Nat-like types to big ints+  --no-optimise-nat-like-types,--no-optimize-nat-like-types+                           Do not compile Nat-like types to big ints   --consolewidth WIDTH     Select console width: auto, infinite, nat   --highlight              Emit source code highlighting   --no-tactic-deprecation-warnings

@@ -110,12 +110,14 @@ void alloc_heap(Heap * h, size_t heap_size, size_t growth, char * old) {     char * mem = malloc(heap_size);+     if (mem == NULL) {         fprintf(stderr,                 "RTS ERROR: Unable to allocate heap. Requested %zd bytes.\n",                 heap_size);         exit(EXIT_FAILURE);     }+    memset(mem, 0, heap_size);      h->heap = mem;     h->next = aligned_heap_pointer(h->heap);

@@ -72,6 +72,7 @@      vm->max_threads = max_threads;     vm->processes = 0;+    vm->creator = NULL;  #else     global_vm = vm;@@ -131,16 +132,18 @@ Stats terminate(VM* vm) {     Stats stats = vm->stats;     STATS_ENTER_EXIT(stats)-#ifdef HAS_PTHREAD-    free(vm->inbox);-#endif     free(vm->valstack);     free_heap(&(vm->heap));     c_heap_destroy(&(vm->c_heap)); #ifdef HAS_PTHREAD-    pthread_mutex_destroy(&(vm -> inbox_lock));-    pthread_mutex_destroy(&(vm -> inbox_block));-    pthread_cond_destroy(&(vm -> inbox_waiting));+    pthread_mutex_destroy(&(vm->inbox_lock));+    pthread_mutex_destroy(&(vm->inbox_block));+    pthread_mutex_destroy(&(vm->alloc_lock));+    pthread_cond_destroy(&(vm->inbox_waiting));+    free(vm->inbox);+    if (vm->creator != NULL) {+        vm->creator->processes--;+    } #endif     // free(vm);     // Set the VM as inactive, so that if any message gets sent to it@@ -209,7 +212,6 @@ }  void* iallocate(VM * vm, size_t isize, int outerlock) {-//    return malloc(isize);     size_t size = aligned(isize);  #ifdef HAS_PTHREAD@@ -225,7 +227,6 @@         char* ptr = vm->heap.next;         vm->heap.next += size;         assert(vm->heap.next <= vm->heap.end);-        memset(ptr, 0, size);         ((Hdr*)ptr)->sz = isize;  #ifdef HAS_PTHREAD@@ -783,28 +784,25 @@     return MKSTR(vm, ""); } +#ifdef HAS_PTHREAD typedef struct {     VM* vm; // thread's VM-    VM* callvm; // calling thread's VM     func fn;     VAL arg; } ThreadData; -#ifdef HAS_PTHREAD void* runThread(void* arg) {     ThreadData* td = (ThreadData*)arg;     VM* vm = td->vm;-    VM* callvm = td->callvm;+    func fn = td->fn;      init_threaddata(vm);      TOP(0) = td->arg;     BASETOP(0);     ADDTOP(1);-    td->fn(vm, NULL);-    callvm->processes--;-     free(td);+    fn(vm, NULL);      //    Stats stats =     terminate(vm);@@ -816,6 +814,7 @@     VM* vm = init_vm(callvm->stack_max - callvm->valstack, callvm->heap.size,                      callvm->max_threads);     vm->processes=1; // since it can send and receive messages+    vm->creator = callvm;     pthread_t t;     pthread_attr_t attr; //    size_t stacksize;@@ -824,15 +823,15 @@ //    pthread_attr_getstacksize (&attr, &stacksize); //    pthread_attr_setstacksize (&attr, stacksize*64); -    ThreadData *td = malloc(sizeof(ThreadData));+    ThreadData *td = malloc(sizeof(ThreadData)); // free'd in runThread     td->vm = vm;-    td->callvm = callvm;     td->fn = f;     td->arg = copyTo(vm, arg);      callvm->processes++;      int ok = pthread_create(&t, &attr, runThread, td);+    pthread_attr_destroy(&attr); //    usleep(100);     if (ok == 0) {         return vm;@@ -843,7 +842,7 @@ }  void* idris_stopThread(VM* vm) {-    close_vm(vm);+    terminate(vm);     pthread_exit(NULL);     return NULL; }

@@ -4,8 +4,8 @@ #include <assert.h> #include <stdlib.h> #include <stdio.h>-#ifdef HAS_PTHREAD #include <string.h>+#ifdef HAS_PTHREAD #include <stdarg.h> #include <pthread.h> #endif@@ -152,6 +152,7 @@      int processes; // Number of child processes     int max_threads; // maximum number of threads to run in parallel+    struct VM* creator; // The VM that created this VM, NULL for root VM #endif     Stats stats; @@ -331,7 +332,7 @@ #define PROJECT(vm,r,loc,num) \     memcpy(&(LOC(loc)), ((Con*)(r))->args, sizeof(VAL)*num) #define SLIDE(vm, args) \-    memcpy(&(LOC(0)), &(TOP(0)), sizeof(VAL)*args)+    memmove(&(LOC(0)), &(TOP(0)), sizeof(VAL)*args)  void* iallocate(VM *, size_t, int); 

@@ -11,9 +11,7 @@ #include <unistd.h>  #ifdef _WIN32-int win_fpoll(void* h);-FILE *win32_u8fopen(const char *path, const char *mode);-FILE *win32_u8popen(const char *path, const char *mode);+#include "windows/win_utils.h" #else #include <sys/select.h> #endif@@ -48,6 +46,10 @@     return ferror(f); } +int fileRemove(const char *filename) {+    return remove(filename);+}+ int fileSize(void* h) {     FILE* f = (FILE*)h;     int fd = fileno(f);@@ -108,6 +110,7 @@     } else {         DirInfo* di = malloc(sizeof(DirInfo));         di->dirptr = d;+        di->error = 0;          return (void*)di;     }@@ -203,6 +206,26 @@ VAL idris_time() {     time_t t = time(NULL);     return MKBIGI(t);+}++VAL idris_clock(VM* vm) {+    VAL result;+#ifdef _WIN32+    int64_t sec, nsec;+    win32_gettime(&sec, &nsec);+    idris_constructor(result, vm, 0, 2, 0);+    idris_setConArg(result, 0, MKBIGI(sec));+    idris_setConArg(result, 1, MKBIGI(nsec));+#else+    struct timespec ts;+    // We're not checking the result here, which is of course bad, but+    // CLOCK_REALTIME is required by POSIX at least!+    clock_gettime(CLOCK_REALTIME, &ts);+    idris_constructor(result, vm, 0, 2, 0);+    idris_setConArg(result, 0, MKBIGI(ts.tv_sec));+    idris_setConArg(result, 1, MKBIGI(ts.tv_nsec));+#endif+    return result; }  VAL idris_mkFileError(VM* vm) {

@@ -12,6 +12,7 @@ void fileClose(void* h); int fileEOF(void* h); int fileError(void* h);+int fileRemove(const char* fname); // Returns a negative number if not a file (e.g. directory or device) int fileSize(void* h); @@ -52,6 +53,7 @@ char* getEnvPair(int i);  VAL idris_time();+VAL idris_clock(VM* vm);  void idris_forceGC(); 

@@ -0,0 +1,43 @@+cmake_minimum_required(VERSION 3.7.2)++project(libsel4-idris-rts C)++file(GLOB static+    rts/idris_rts.c+    rts/idris_heap.c+    rts/idris_gc.c+    rts/idris_gmp.c+    rts/idris_bitstring.c+    rts/idris_opts.c+    rts/idris_stats.c+    rts/idris_utf8.c+    rts/idris_stdfgn.c+    rts/mini-gmp.c+    rts/idris_buffer.c+    rts/getline.c+    rts/idris_net.c+    rts/seL4/idris_main.c+)++set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wall")+# Ignore some warnings+set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wno-unused-parameter")+set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wno-sign-compare")+# Don't use the host machines' environment when cross compiling+set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -undef")+set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -DIDRIS_TARGET_OS=\"\\\"seL4\\\"\"")+set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -DSEL4")+execute_process(+    COMMAND ${CMAKE_C_COMPILER} -dumpmachine+    OUTPUT_VARIABLE MACHINE+    OUTPUT_STRIP_TRAILING_WHITESPACE+)+set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -DIDRIS_TARGET_TRIPLE=\"\\\"${MACHINE}\\\"\"")++add_library(sel4-idris-rts EXCLUDE_FROM_ALL ${static})+target_include_directories(sel4-idris-rts PUBLIC rts)+target_link_libraries(+    sel4-idris-rts+    Configuration+    muslc+)

@@ -1,2 +0,0 @@-libsel4-idris-rts: $(libc) common-libs-$(CONFIG_LIBSEL4_IDRIS_RTS) += libsel4-idris-rts

@@ -1,9 +0,0 @@-config LIBSEL4_IDRIS_RTS-    bool "libsel4-idris-rts"-    default y-    select HAVE_LIBSEL4_IDRIS_RTS-    help-        Idris RTS compiled for seL4--config HAVE_LIBSEL4_IDRIS_RTS-    bool

@@ -1,33 +0,0 @@-# Target-TARGETS := libsel4-idris-rts.a--# Source files required to build the target-FILES := \-    idris_rts.c \-    idris_heap.c \-    idris_gc.c \-    idris_gmp.c \-    idris_bitstring.c \-    idris_opts.c \-    idris_stats.c \-    idris_utf8.c \-    idris_stdfgn.c \-    mini-gmp.c \-    idris_buffer.c \-    getline.c \-    idris_net.c \-    seL4/idris_main.c-CFILES := $(addprefix rts/,$(FILES))--# Header file directory this library provides-HDRFILES := $(wildcard ${SOURCE_DIR}/rts/*)--CFLAGS += -W -Wall-# Don't use the host machines' environment when cross compiling-CFLAGS += -undef-CFLAGS += -DIDRIS_TARGET_OS=\"seL4\"-CFLAGS += -DSEL4-MACHINE := $(shell $(CC) -dumpmachine)-CFLAGS += -DIDRIS_TARGET_TRIPLE=\"$(MACHINE)\"--include $(SEL4_COMMON)/common.mk

@@ -0,0 +1,5 @@+# libsel4-idris-rts - Idris RTS library for the seL4 microkernel+The Idris RTS compiled to the seL4 microkernel.++## How to use this library?+See the instructions in the project repository, [mokshasoft/sel4-idris-manifest](https://github.com/mokshasoft/sel4-idris-manifest).

@@ -6,8 +6,8 @@ void _idris__123_runMain_95_0_125_(VM* vm, VAL* oldbase);  RTSOpts opts = {-    .init_heap_size = 16384000,-    .max_stack_size = 4096000,+    .init_heap_size = 100000,+    .max_stack_size = 5000,     .show_summary   = 0 }; @@ -24,7 +24,6 @@     } #endif -    free_nullaries();     // Remove call to terminate since it crashes the application during a free     //Stats stats = terminate(vm); 

@@ -1,7 +1,9 @@ #include <io.h>+#include <stdint.h> #include <stdio.h> #include <windows.h> + // THis file exists to avoid clashes between windows.h and idris_rts.h // @@ -28,6 +30,7 @@     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;@@ -48,4 +51,17 @@     free(wpath);     free(wmode);     return f;+}++void win32_gettime(int64_t* sec, int64_t* nsec)+{+    FILETIME ft;+    GetSystemTimePreciseAsFileTime(&ft);+    ULARGE_INTEGER t;+    t.HighPart = ft.dwHighDateTime;+    t.LowPart = ft.dwLowDateTime;++    *nsec = (t.QuadPart % 10000000)*100;+    *sec = t.QuadPart / 10000000;+    *sec -= 11644473600; // LDAP epoch to Unix epoch  }

@@ -0,0 +1,9 @@+#include <stdint.h>+#include <stdio.h>++#pragma once++int win_fpoll(void *h);+FILE *win32_u8fopen(const char *path, const char *mode);+FILE *win32_u8popen(const char *path, const char *mode);+void win32_gettime(int64_t* sec, int64_t* nsec);

@@ -72,6 +72,7 @@            Raw -> writeSource out cout            _ -> do              (tmpn, tmph) <- tempfile ".c"+             hSetEncoding tmph utf8              hPutStr tmph cout              hFlush tmph              hClose tmph@@ -121,7 +122,7 @@  cname :: Name -> String cname n = "_idris_" ++ concatMap cchar (showCG n)-  where cchar x | isAlpha x || isDigit x = [x]+  where cchar x | isAscii x && isAlpha x || isDigit x = [x]                 | otherwise = "_" ++ show (fromEnum x) ++ "_"  indent :: Int -> String

@@ -5,7 +5,8 @@ License     : BSD3 Maintainer  : The Idris Community. -}-{-# LANGUAGE CPP, FlexibleContexts, PatternGuards, TypeSynonymInstances #-}+{-# LANGUAGE CPP, FlexibleContexts, MultiWayIf, NamedFieldPuns, PatternGuards,+             TypeSynonymInstances #-}  module IRTS.Compiler(compile, generate) where @@ -34,6 +35,7 @@ import Control.Monad.State import Data.List import qualified Data.Map as M+import Data.Maybe (maybe) import Data.Ord import qualified Data.Set as S import System.Directory@@ -393,6 +395,16 @@             EQ  | isNewtype                 -> irTerm top vs env (head argsPruned) +                -- compile Nat-likes as bigints+                | Just LikeZ <- isLikeNat ist n+                -> irTerm top vs env $ Constant (BI 0)++                -- compile Nat-likes as bigints+                | Just LikeS <- isLikeNat ist n+                -> irTerm top vs env $ mkApp+                    (P Ref (sUN "prim__addBigInt") Erased)+                    (Constant (BI 1) : argsPruned)+                 | otherwise  -- not newtype, plain data ctor                 -> buildApp (LV n) argsPruned @@ -405,6 +417,14 @@                 | isNewtype  -- newtype but the value is not among args yet                 -> return . padLams $ \[vn] -> LApp False (LV n) [LV vn] +                -- compile Nat-likes as bigints+                -- it seems that prim applications needn't be saturated+                | Just LikeS <- isLikeNat ist n+                -> irTerm top vs env $+                    App Complete+                        (P Ref (sUN "prim__addBigInt") Erased)+                        (Constant $ BI 1)+                 -- not a newtype, just apply to a constructor                 | otherwise                 -> padLams . applyToNames <$> buildApp (LV n) argsPruned@@ -501,6 +521,58 @@ irTerm top vs env Erased              = return LNothing irTerm top vs env Impossible          = return LNothing +data LikeNat = LikeZ | LikeS++isLikeNat :: IState -> Name -> Maybe LikeNat+isLikeNat ist cn+    -- Nat itself is special-cased in Idris/DataOpts.hs,+    -- which will have already happened at this point.++    -- If the optimisation is disabled then nothing looks like Nat.+    | GeneralisedNatHack `notElem` opt_optimise (idris_options ist)+    = Nothing++    | Just cTy <- lookupTyExact cn $ tt_ctxt ist+    , (P TCon{} tyN _, _) <- unApply $ getRetTy cTy+    , Just (z, s) <- natLikeCtors tyN+    = if | cn == z -> Just LikeZ+         | cn == s -> Just LikeS+         | otherwise -> error $ "isLikeNat: constructor not found in its own family: " ++ show (cn, tyN)++    | otherwise = Nothing+  where+    natLikeCtors :: Name -> Maybe (Name, Name)+    natLikeCtors tyN = case lookupCtxtExact tyN $ idris_datatypes ist of+        Just TI{con_names = [z, s]}+            | 0 <- getUsedCount z+            , looksLikeS s+            -> Just (z, s)++        Just TI{con_names = [s, z]}+            | 0 <- getUsedCount z+            , looksLikeS s+            -> Just (z, s)++        _ -> Nothing++    getUsedCount :: Name -> Int+    getUsedCount n =+        maybe 0 (length . usedpos)+        $ lookupCtxtExact n+        $ idris_callgraph ist++    looksLikeS :: Name -> Bool+    looksLikeS cn+        | Just [(i, _)] <- fmap usedpos $ lookupCtxtExact cn $ idris_callgraph ist+        , Just cTy <- lookupTyExact cn $ tt_ctxt ist+        , [recTy] <- [recTy | (j, (_n, recTy)) <- zip [0..] (getArgTys cTy), j == i]+        , (P TCon{} recTyN _, _) <- unApply recTy+        , (P TCon{} tyN _, _) <- unApply $ getRetTy cTy+        , recTyN == tyN+        = True++        | otherwise = False+ doForeign :: Vars -> [Name] -> [Term] -> Idris LExp doForeign vs env (ret : fname : world : args)      = do args' <- mapM splitArg args@@ -533,7 +605,7 @@  irSC :: Name -> Vars -> SC -> Idris LExp irSC top vs (STerm t) = irTerm top vs [] t-irSC top vs (UnmatchedCase str) = return $ LLazyExp $ LError str+irSC top vs (UnmatchedCase str) = return $ LError str  irSC top vs (ProjCase tm alts) = do     tm'   <- irTerm top vs [] tm@@ -616,18 +688,41 @@     detag <- fgetState (opt_detaggable . ist_optimisation cn)     if detag         then irSC top vs (Case up n [ConCase cn a ns sc])-        else LCase up (LV n) <$> mapM (irAlt top vs (LV n)) alts+        else do+            likeNat <- isLikeNat <$> getIState <*> pure cn+            case likeNat of+                -- the annoying case: LikeS is translated into a default case+                -- so we need to change the original DefaultCase to Z-case+                -- and reorder it before this one+                Just LikeS -> do+                    zCase <- LConstCase (BI 0) <$> irSC top vs sc'+                    sCase <- irAlt top vs (LV n) (ConCase cn a ns sc)+                    return $ LCase up (LV n) [zCase, sCase] -irSC top vs sc@(Case up n alts) = do-    -- check that neither alternative needs the newtype optimisation,-    -- see comment above-    goneWrong <- or <$> mapM isDetaggable alts-    when goneWrong-        $ ifail ("irSC: non-trivial case-match on detaggable data: " ++ show sc)+                -- the usual case+                _ -> LCase up (LV n) <$> mapM (irAlt top vs (LV n)) alts -    -- everything okay-    LCase up (LV n) <$> mapM (irAlt top vs (LV n)) alts+irSC top vs sc@(Case up n alts) = getIState >>= rhs   where+    rhs ist+        | [ConCase cns as nss scs, ConCase cnz az nsz scz] <- alts+        , Just LikeS <- isLikeNat ist cns+        = do+            -- reorder to make the Z case come first+            zCase <- LConstCase (BI 0) <$> irSC top vs scz+            sCase <- irAlt top vs (LV n) (ConCase cns as nss scs)+            return $ LCase up (LV n) [zCase, sCase]++        | otherwise = do+            -- check that neither alternative needs the newtype optimisation,+            -- see comment above+            goneWrong <- or <$> mapM isDetaggable alts+            when goneWrong+                $ ifail ("irSC: non-trivial case-match on detaggable data: " ++ show sc)++            -- everything okay+            LCase up (LV n) <$> mapM (irAlt top vs (LV n)) alts+     isDetaggable (ConCase cn _ _ _) = fgetState $ opt_detaggable . ist_optimisation cn     isDetaggable  _                 = return False @@ -636,10 +731,32 @@ irAlt :: Name -> Vars -> LExp -> CaseAlt -> Idris LAlt  -- this leaves out all unused arguments of the constructor-irAlt top vs _ (ConCase n t args sc) = do+irAlt top vs tm (ConCase n t args sc) = do+    likeNat <- isLikeNat <$> getIState <*> pure n     used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)     let usedArgs = [a | (i,a) <- zip [0..] args, i `elem` used]-    LConCase (-1) n usedArgs <$> irSC top (methodVars `M.union` vs) sc++    case likeNat of+        -- like S+        Just LikeS -> do+            sc' <- irSC top vs sc+            case usedArgs of+                [pv] -> return $ LDefaultCase $ LLet pv+                        ( LOp+                            (LMinus (ATInt ITBig))+                            [ tm+                            , LConst (BI 1)+                            ]+                        )+                        sc'++                _ -> ifail $ "irAlt/LikeS: multiple used args: " ++ show usedArgs++        -- like Z+        Just LikeZ -> LConstCase (BI 0) <$> irSC top vs sc++        -- not like Nat+        Nothing -> LConCase (-1) n usedArgs <$> irSC top (methodVars `M.union` vs) sc   where     methodVars = case n of         SN (ImplementationCtorN interfaceName)

@@ -202,7 +202,7 @@     default2Text Nothing = ""     default2Text (Just z) =       T.concat ["default:\n", indent $ T.concat [jsStmt2Text z, ";\nbreak;\n"]]-jsStmt2Text (JsError t) = T.concat ["throw new Error(  ", jsAst2Text t, ");"]+jsStmt2Text (JsError t) = T.concat ["$JSRTS.die(", jsAst2Text t, ");\n"] jsStmt2Text (JsForever x) =   T.concat ["for(;;) {\n", indent $ jsStmt2Text x, "}\n"] jsStmt2Text JsContinue = "continue;"

@@ -108,22 +108,25 @@ makeExportDecls defs (Export _ _ e) =   concatMap makeExport e   where-    uncurryF name argTy (Just args) =-      if length argTy == length args then name+    uncurryF name argTy (Just args) retTy =+      if length argTy == length args then+          case (retTy, length args) of+            (FIO _, 0) -> T.concat ["function(){return ", name, "()()}"]+            _ -> name         else T.concat [ "function(){ return "                       , name                       , ".apply(this, Array.prototype.slice.call(arguments, 0,", T.pack $ show $ length args,"))"                       , T.concat $ map (\x -> T.concat ["(arguments[", T.pack $ show x , "])"]) [length args .. (length argTy - 1)]                       , "}"                       ]-    uncurryF name argTy Nothing = name+    uncurryF name argTy Nothing retTy = name      makeExport (ExportData _) =       []     makeExport (ExportFun name (FStr exportname) retTy argTy) =       [T.concat [ T.pack $ exportname                 ,  ": "-                , uncurryF (jsName name) argTy (getArgList' name defs)+                , uncurryF (jsName name) argTy (getArgList' name defs) retTy                 ]       ] 

@@ -1659,7 +1659,8 @@             argInfo n (Imp opt _ _ _ _ _) Placeholder                    = (True, PImp 0 True opt n Placeholder)             argInfo n (Imp opt _ _ _ _ _) t'-                   = (False, PImp (getPriority i t') True opt n t')+                   = (InaccessibleArg `elem` opt,+                          PImp (getPriority i t') True opt n t')             argInfo n (Exp opt _ _ _) t'                    = (InaccessibleArg `elem` opt,                           PExp (getPriority i t') opt n t')

@@ -392,6 +392,7 @@               | IBCDeprecate Name String               | IBCFragile Name String               | IBCConstraint FC UConstraint+              | IBCImportHash FilePath Int   deriving (Show, Generic)  initialInteractiveOpts :: InteractiveOpts

@@ -209,6 +209,17 @@   <|> flag' (AddOpt PETransform) (long "partial-eval")   <|> flag' (RemoveOpt PETransform) (long "no-partial-eval" <> help "Switch off partial evaluation, mainly for debugging purposes") +  <|> flag' (AddOpt GeneralisedNatHack) (+    long "optimise-nat-like-types"+    <> long "optimize-nat-like-types"+    <> help "Enable compilation of Nat-like types to bigints"+  )+  <|> flag' (RemoveOpt GeneralisedNatHack) (+    long "no-optimise-nat-like-types"+    <> long "no-optimize-nat-like-types"+    <> help "Disable compilation of Nat-like types to bigints"+  )+   <|> OptLevel <$> option auto (short 'O' <> long "level")    <|> TargetTriple <$> strOption (long "target" <> metavar "TRIPLE" <> help "If supported the codegen will target the named triple.")

@@ -24,6 +24,7 @@                 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,                 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,                 mapDefCtxt, tcReducible,+                lookupTotalAccessibility,                 lookupTotal, lookupTotalExact, lookupInjectiveExact,                 lookupRigCount, lookupRigCountExact,                 lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict,@@ -1166,6 +1167,12 @@   -- 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)++lookupTotalAccessibility :: Name -> Context -> [(Totality,Accessibility)]+lookupTotalAccessibility n ctxt = fmap unpack $ lookupCtxt n (definitions ctxt)++  where+    unpack ((_,_,_,a,t,_)) = (t,a)  lookupDefAccExact :: Name -> Bool -> Context ->                      Maybe (Def, Accessibility)

@@ -30,6 +30,7 @@ import Data.Time.Clock.POSIX (getPOSIXTime) import Data.Traversable (forM) import Debug.Trace+import System.Directory import System.IO import System.IO.Error import System.IO.Unsafe@@ -345,7 +346,7 @@            = case (fileStr, modeStr) of                (EConstant (Str f), EConstant (Str mode)) ->                  do f <- execIO $-                         catch (do let m = case mode of+                         catch (do let m = case filter (/= 'b') mode of                                              "r"  -> Right ReadMode                                              "w"  -> Right WriteMode                                              "a"  -> Right AppendMode@@ -386,6 +387,17 @@                _ -> execFail . Msg $                       "The argument to fileError should be a file handle, but it was " ++                       show handle +++                      ". Are all cases covered?"+    | Just (FFun "fileRemove" [(_,fileStr)] _) <- foreignFromTT arity ty fn xs+           = case fileStr of+               EConstant (Str f) -> do res <- execIO $ catch (do removeFile f+                                                                 return $ ioWrap $ EConstant $ I 0)+                                                             (\e -> do writeIORef fileError $ mapError e+                                                                       return $ ioWrap $ EConstant $ I (-1))+                                       execApp env ctxt res (drop arity xs)+               _ -> execFail . Msg $+                      "The argument to fileRemove should be a constant string, but it was " +++                      show fileStr ++                       ". Are all cases covered?"     | Just (FFun "fileClose" [(_,handle)] _) <- foreignFromTT arity ty fn xs            = case handle of

@@ -94,11 +94,9 @@            (if not (null argshow)              then nest 4 $ text "Arguments:" <$> vsep argshow              else empty)-      -- show totality status-      <> let totality = getTotality in-           (if totalityFlag && not (null totality)-              then line <> (vsep . map (\t -> text "The function is" <+> t) $ totality)-              else empty))+      -- show totality and visibility status+      <> showTotalVisibility+      )      where       ppo = ppOptionIst ist@@ -135,7 +133,14 @@             showArgs args ((n, True):bnd)       showArgs []                                    _   = [] -- end of arguments -      getTotality = map (text . show) $ lookupTotal n (tt_ctxt ist)+      showTotalVisibility =+        case lookupTotalAccessibility n (tt_ctxt ist) of+          [] -> empty+          xs -> line <> vsep (map (doShowTotalVisibility) xs)++      doShowTotalVisibility (t,v) = if totalityFlag+                                       then text "The function is:" <+> ((text . show) t) <+> (text "&") <+> ((text . show) v)+                                       else text "The function is:" <+> ((text . show) v)  pprintFDWithTotality :: IState -> Bool -> FunDoc -> Doc OutputAnnotation pprintFDWithTotality ist = pprintFD ist True

@@ -660,11 +660,13 @@         i <- getIState         inf <- isTyInferred fname -        -- Check if we have "with" patterns outside of "with" block-        when (isOutsideWith lhs_in && (not $ null withs)) $+        -- Check if we have extra "with" patterns+        when (not $ null withs) $             ierror (At (fromMaybe NoFC $ highestFC lhs_in_as)                        (Elaborating "left hand side of " fname Nothing-                        (Msg "unexpected patterns outside of \"with\" block")))+                        (Msg $ if isOutsideWith lhs_in+                               then "unexpected patterns outside of \"with\" block"+                               else "unexpected extra \"with\" patterns")))          -- get the parameters first, to pass through to any where block         let fn_ty = case lookupTy fname ctxt of

@@ -12,7 +12,8 @@  module Idris.IBC (loadIBC, loadPkgIndex,                   writeIBC, writePkgIndex,-                  hasValidIBCVersion, IBCPhase(..)) where+                  hasValidIBCVersion, IBCPhase(..),+                  getIBCHash, getImportHashes) where  import Idris.AbsSyntax import Idris.Core.CaseTree@@ -40,7 +41,7 @@ import System.FilePath  ibcVersion :: Word16-ibcVersion = 165+ibcVersion = 166  -- | When IBC is being loaded - we'll load different things (and omit -- different structures/definitions) depending on which phase we're in.@@ -50,6 +51,7 @@  data IBCFile = IBCFile {     ver                        :: Word16+  , iface_hash                 :: Int   , sourcefile                 :: FilePath   , ibc_imports                :: ![(Bool, FilePath)]   , ibc_importdirs             :: ![FilePath]@@ -101,6 +103,7 @@   , ibc_fragile                :: ![(Name, String)]   , ibc_constraints            :: ![(FC, UConstraint)]   , ibc_langexts               :: ![LanguageExt]+  , ibc_importhashes           :: ![(FilePath, Int)]   }   deriving Show {-!@@ -108,7 +111,7 @@ !-}  initIBC :: IBCFile-initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] [] [] [] []+initIBC = IBCFile ibcVersion 0 "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] [] [] [] [] []  hasValidIBCVersion :: FilePath -> Idris Bool hasValidIBCVersion fp = do@@ -143,6 +146,21 @@                                 else unhide phase fp archive                             addImported reexport fp +getIBCHash :: FilePath -> Idris Int+getIBCHash fp+    = do archiveFile <- runIO $ B.readFile fp+         case toArchiveOrFail archiveFile of+              Left _ -> return 0+              Right archive -> getEntry 0 "iface_hash" archive+++getImportHashes :: FilePath -> Idris [(FilePath, Int)]+getImportHashes fp+    = do archiveFile <- runIO $ B.readFile fp+         case toArchiveOrFail archiveFile of+              Left _ -> return []+              Right archive -> getEntry [] "ibc_importhashes" archive+ -- | Load an entire package from its index file loadPkgIndex :: PkgName -> Idris () loadPkgIndex pkg = do ddir <- runIO getIdrisLibDir@@ -159,6 +177,7 @@  entries :: IBCFile -> [Entry] entries i = catMaybes [Just $ toEntry "ver" 0 (encode $ ver i),+                       Just $ toEntry "iface_hash" 0 (encode $ iface_hash i),                        makeEntry "sourcefile"  (sourcefile i),                        makeEntry "ibc_imports"  (ibc_imports i),                        makeEntry "ibc_importdirs"  (ibc_importdirs i),@@ -208,7 +227,8 @@                        makeEntry "ibc_injective"  (ibc_injective i),                        makeEntry "ibc_access"  (ibc_access i),                        makeEntry "ibc_fragile" (ibc_fragile i),-                       makeEntry "ibc_langexts" (ibc_langexts i)]+                       makeEntry "ibc_langexts" (ibc_langexts i),+                       makeEntry "ibc_importhashes" (ibc_importhashes i)] -- TODO: Put this back in shortly after minimising/pruning constraints --                        makeEntry "ibc_constraints" (ibc_constraints i)] @@ -223,14 +243,73 @@          iReport 2 $ "Writing IBC for: " ++ show f          i <- getIState          resetNameIdx-         ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src,-                                                ibc_langexts = idris_language_extensions i })+         ibc_data <- mkIBC (ibc_write i) (initIBC { sourcefile = src,+                                                    ibc_langexts = idris_language_extensions i })+         let ibcf = ibc_data { iface_hash = calculateHash i ibc_data }+         logIBC 5 $ "Hash for " ++ show f ++ " = " ++ show (iface_hash ibcf)          idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)                         writeArchive f ibcf                         logIBC 2 "Written")             (\c -> do logIBC 2 $ "Failed " ++ pshow i c)          return () +qhash :: Int -> String -> Int+qhash hash [] = abs hash `mod` 0xffffffff+qhash hash (x:xs) = qhash (hash * 33 + fromIntegral (fromEnum x)) xs++hashTerm :: Int -> Term -> Int+hashTerm i t = qhash (i * 5381) (show t)++hashName :: Int -> Name -> Int+hashName i n = qhash (i * 5381) (show n)++calculateHash :: IState -> IBCFile -> Int+calculateHash ist f+    = let acc = L.filter exported (ibc_access f)+          inl = L.filter (inlinable (map fst acc)) (ibc_flags f) in+          mkHashFrom (map fst acc) (getDefs acc ++ L.concatMap getFullDef inl)+  where+    mkHashFrom :: [Name] -> [Term] -> Int+    mkHashFrom ns tms = sum (L.zipWith hashName [1..] ns) ++                        sum (L.zipWith hashTerm [1..] tms)++    exported (_, Public) = True+    exported (_, Frozen) = True+    exported _ = False++    inlinable acc (n, opts)+        = n `elem` acc &&+             (Inlinable `elem` opts || PEGenerated `elem` opts)++    findTms :: [(a, Term, Term)] -> [Term]+    findTms = L.concatMap (\ (_, x, y) -> [x, y])++    patDef :: Name -> [Term]+    patDef n+        = case lookupCtxtExact n (idris_patdefs ist) of+               Nothing -> []+               Just (tms, _) -> findTms tms++    getDefs :: [(Name, Accessibility)] -> [Term]+    getDefs [] = []+    getDefs ((n, Public) : ns)+        = let ts = getDefs ns in+              case lookupTyExact n (tt_ctxt ist) of+                   Nothing -> ts+                   Just ty -> ty : patDef n ++ ts+    getDefs ((n, Frozen) : ns)+        = let ts = getDefs ns in+              case lookupTyExact n (tt_ctxt ist) of+                   Nothing -> ts+                   Just ty -> ty : ts+    getDefs (_ : ns) = getDefs ns++    getFullDef :: (Name, [FnOpt]) -> [Term]+    getFullDef (n, _)+        = case lookupTyExact n (tt_ctxt ist) of+               Nothing -> []+               Just ty -> ty : patDef n+ -- | Write a package index containing all the imports in the current -- IState Used for ':search' of an entire package, to ensure -- everything is loaded.@@ -347,6 +426,7 @@ ibc i (IBCDeprecate n r) f = return f { ibc_deprecated = (n, r) : ibc_deprecated f } ibc i (IBCFragile n r)   f = return f { ibc_fragile    = (n,r)  : ibc_fragile f } ibc i (IBCConstraint fc u)  f = return f { ibc_constraints = (fc, u) : ibc_constraints f }+ibc i (IBCImportHash fn h) f = return f { ibc_importhashes = (fn, h) : ibc_importhashes f }  getEntry :: (Binary b, NFData b) => b -> FilePath -> Archive -> Idris b getEntry alt f a = case findEntryByPath f a of

@@ -125,7 +125,7 @@  data OutputFmt = HTMLOutput | LaTeXOutput -data Optimisation = PETransform -- ^ partial eval and associated transforms+data Optimisation = PETransform | GeneralisedNatHack -- ^ partial eval and associated transforms   deriving (Show, Eq, Generic)  -- | Recognised logging categories for the Idris compiler.

@@ -75,9 +75,10 @@ formatMessage :: Message w => w -> Idris OutputDoc formatMessage w = do     i <- getIState-    maybeSource <- case messageSource w of-                     Just src -> pure (Just src)-                     Nothing  -> readSource fc+    rs <- readSource fc+    let maybeSource = case rs of+          Just src -> Just src+          Nothing -> messageSource w     let maybeFormattedSource = maybeSource >>= layoutSource fc (regions (idris_highlightedRegions i))     return $ layoutMessage (layoutFC fc) maybeFormattedSource (messageText w)   where

@@ -13,9 +13,10 @@ import Idris.Options (Opt) import Idris.Package.Common import Idris.Parser (moduleName)-import Idris.Parser.Helpers (Parser, Parsing, eol, iName, identifier, isEol,-                             lchar, packageName, parseErrorDoc, reserved,-                             runparser, someSpace, stringLiteral)+import Idris.Parser.Helpers (Parser, Parsing, eol, iName, identifier,+                             identifierWithExtraChars, isEol, lchar,+                             packageName, parseErrorDoc, reserved, runparser,+                             someSpace, stringLiteral)  import Control.Applicative import Control.Monad.State.Strict@@ -26,14 +27,13 @@ import System.FilePath (isValid, takeExtension, takeFileName) import Text.Megaparsec ((<?>)) import qualified Text.Megaparsec as P-import qualified Text.Megaparsec.Char as P import qualified Text.PrettyPrint.ANSI.Leijen as PP  type PParser = Parser PkgDesc  parseDesc :: FilePath -> IO PkgDesc parseDesc fp = do-    when (not $ takeExtension fp == ".ipkg") $ do+    unless (takeExtension fp == ".ipkg") $ do         putStrLn $ unwords ["The presented iPKG file does not have a '.ipkg' extension:", show fp]         exitWith (ExitFailure 1)     res <- doesFileExist fp@@ -119,17 +119,20 @@     Opts.Failure e -> fail $ fst $ Opts.renderFailure e ""     _              -> fail "Unexpected error" +libIdentifier :: Parsing m => m String+libIdentifier = identifierWithExtraChars "_'-."+ pClause :: PParser () pClause = clause "executable" filename (\st v -> st { execout = Just v })       <|> clause "main" (iName []) (\st v -> st { idris_main = Just v })-      <|> clause "sourcedir" identifier (\st v -> st { sourcedir = v })+      <|> clause "sourcedir" (identifier <|> stringLiteral) (\st v -> st { sourcedir = v })       <|> clause "opts" pOptions (\st v -> st { idris_opts = v ++ idris_opts st })       <|> clause "pkgs" (commaSep (pPkgName <* someSpace)) (\st ps ->              let pkgs = pureArgParser $ concatMap (\x -> ["-p", show x]) ps              in st { pkgdeps    = ps `union` pkgdeps st                    , idris_opts = pkgs ++ idris_opts st })       <|> clause "modules" (commaSep moduleName) (\st v -> st { modules = modules st ++ v })-      <|> clause "libs" (commaSep identifier) (\st v -> st { libdeps = libdeps st ++ v })+      <|> clause "libs" (commaSep libIdentifier) (\st v -> st { libdeps = libdeps st ++ v })       <|> clause "objs" (commaSep identifier) (\st v -> st { objs = objs st ++ v })       <|> clause "makefile" (iName []) (\st v -> st { makefile = Just (show v) })       <|> clause "tests" (commaSep (iName [])) (\st v -> st { idris_tests = idris_tests st ++ v })@@ -142,3 +145,4 @@       <|> clause "brief" stringLiteral (\st v -> st { pkgbrief = Just v })       <|> clause "author" textUntilEol (\st v -> st { pkgauthor = Just v })       <|> clause "maintainer" textUntilEol (\st v -> st { pkgmaintainer = Just v })+

@@ -55,11 +55,11 @@ import Data.Ord import qualified Data.Set as S import qualified Data.Text as T-import qualified System.Directory as Dir (makeAbsolute)+import qualified System.Directory as Dir (doesFileExist, getModificationTime,+                                          makeAbsolute) import System.FilePath import Text.Megaparsec ((<?>)) import qualified Text.Megaparsec as P-import qualified Text.Megaparsec.Char as P import qualified Text.PrettyPrint.ANSI.Leijen as PP  {-@@ -1640,162 +1640,196 @@ {-| Load Idris source code-} loadSource :: Bool -> FilePath -> Maybe Int -> Idris () loadSource lidr f toline-             = do logParser 1 ("Reading " ++ f)-                  iReport   2 ("Reading " ++ f)-                  i <- getIState-                  let def_total = default_total i-                  file_in <- runIO $ readSource f-                  file <- if lidr then tclift $ unlit f file_in else return file_in-                  (mdocs, mname, imports_in, pos) <- parseImports f file-                  ai <- getAutoImports-                  let imports = map (\n -> ImportInfo True n Nothing [] NoFC NoFC) ai ++ imports_in-                  ids <- rankedImportDirs f-                  ibcsd <- valIBCSubDir i-                  mapM_ (\(re, f, ns, nfc) ->-                               do fp <- findImport ids ibcsd f-                                  case fp of-                                      LIDR fn -> ifail $ "No ibc for " ++ f-                                      IDR fn -> ifail $ "No ibc for " ++ f-                                      IBC fn src ->-                                        do loadIBC True IBC_Building fn-                                           let srcFn = case src of-                                                         IDR fn -> Just fn-                                                         LIDR fn -> Just fn-                                                         _ -> Nothing-                                           srcFnAbs <- case srcFn of-                                                         Just fn -> fmap Just (runIO $ Dir.makeAbsolute fn)-                                                         Nothing -> return Nothing-                                           sendHighlighting $ S.fromList [(FC' nfc, AnnNamespace ns srcFnAbs)])-                        [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports]-                  reportParserWarnings-                  sendParserHighlighting+     = do logParser 1 ("Reading " ++ f)+          iReport   2 ("Reading " ++ f)+          i <- getIState+          let def_total = default_total i+          file_in <- runIO $ readSource f+          file <- if lidr then tclift $ unlit f file_in else return file_in+          (mdocs, mname, imports_in, pos) <- parseImports f file+          ai <- getAutoImports+          let imports = map (\n -> ImportInfo True n Nothing [] NoFC NoFC) ai ++ imports_in+          ids <- rankedImportDirs f+          ibcsd <- valIBCSubDir i+          let ibc = ibcPathNoFallback ibcsd f+          impHashes <- idrisCatch (getImportHashes ibc)+                                  (\err -> return [])+          newHashes <- mapM (\ (_, f, _, _) ->+                         do fp <- findImport ids ibcsd f+                            case fp of+                                 IBC fn src ->+                                   idrisCatch (do hash <- getIBCHash fn+                                                  return (Just (fn, hash)))+                                              (\err -> return Nothing)+                                 _ -> return Nothing)+                [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports] -                  -- process and check module aliases-                  let modAliases = M.fromList-                        [ (prep alias, prep realName)-                        | ImportInfo { import_reexport = reexport-                                     , import_path = realName-                                     , import_rename = Just (alias, _)-                                     , import_location = fc } <- imports-                        ]-                      prep = map T.pack . reverse . Spl.splitOn [pathSeparator]-                      aliasNames = [ (alias, fc)-                                   | ImportInfo { import_rename = Just (alias, fc)-                                                } <- imports-                                   ]-                      histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames-                  case map head . filter ((/= 1) . length) $ histogram of-                    []       -> logParser 3 $ "Module aliases: " ++ show (M.toList modAliases)-                    (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n+          fmod <- liftIO $ Dir.getModificationTime f+          ibcexists <- liftIO $ Dir.doesFileExist ibc+          ibcmod <- if ibcexists+                       then liftIO $ Dir.getModificationTime ibc+                       else return fmod -                  i <- getIState-                  putIState (i { default_access = Private, module_aliases = modAliases })-                  clearIBC -- start a new .ibc file-                  -- record package info in .ibc-                  imps <- allImportDirs-                  mapM_ addIBC (map IBCImportDir imps)-                  mapM_ (addIBC . IBCImport)-                    [ (reexport, realName)+          logParser 10 $ ibc ++ " " ++ show ibcmod+          logParser 10 $ f ++ " " ++ show fmod+          logParser 10 $ show impHashes ++ "\n" ++ show newHashes++          -- If the ibc is newer than the source, and the old import+          -- hashes are the same as the ones we've just read,+          -- quit and just load the IBC++          let needLoad = (ibcmod <= fmod) ||+                         (sort impHashes /= sort (mapMaybe id newHashes))++          if not needLoad+             then pure ()+             else do+              iReport 1 $ "Type checking " ++ f+              mapM_ (\ (re, f, ns, nfc) ->+                           do fp <- findImport ids ibcsd f+                              case fp of+                                  LIDR fn -> ifail $ "No ibc for " ++ f+                                  IDR fn -> ifail $ "No ibc for " ++ f+                                  IBC fn src ->+                                    do loadIBC True IBC_Building fn+                                       let srcFn = case src of+                                                     IDR fn -> Just fn+                                                     LIDR fn -> Just fn+                                                     _ -> Nothing+                                       srcFnAbs <- case srcFn of+                                                     Just fn -> fmap Just (runIO $ Dir.makeAbsolute fn)+                                                     Nothing -> return Nothing+                                       sendHighlighting $ S.fromList [(FC' nfc, AnnNamespace ns srcFnAbs)])+                    [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports]+              reportParserWarnings+              sendParserHighlighting++              -- process and check module aliases+              let modAliases = M.fromList+                    [ (prep alias, prep realName)                     | ImportInfo { import_reexport = reexport                                  , import_path = realName-                                 } <- imports+                                 , import_rename = Just (alias, _)+                                 , import_location = fc } <- imports                     ]-                  let syntax = defaultSyntax{ syn_namespace = reverse mname,-                                              maxline = toline }-                  ist <- getIState-                  -- Save the span from parsing the module header, because-                  -- an empty program parse might obliterate it.-                  let oldSpan = idris_parsedSpan ist-                  ds' <- parseProg syntax f file pos+                  prep = map T.pack . reverse . Spl.splitOn [pathSeparator]+                  aliasNames = [ (alias, fc)+                               | ImportInfo { import_rename = Just (alias, fc)+                                            } <- imports+                               ]+                  histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames+              case map head . filter ((/= 1) . length) $ histogram of+                []       -> logParser 3 $ "Module aliases: " ++ show (M.toList modAliases)+                (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n -                  case (ds', oldSpan) of-                    ([], Just fc) ->-                      -- If no program elements were parsed, we dind't-                      -- get a loaded region in the IBC file. That-                      -- means we need to add it back.-                      do ist <- getIState-                         putIState ist { idris_parsedSpan = oldSpan-                                       , ibc_write = IBCParsedRegion fc :-                                                     ibc_write ist-                                       }-                    _ -> return ()-                  sendParserHighlighting+              i <- getIState+              putIState (i { default_access = Private, module_aliases = modAliases })+              clearIBC -- start a new .ibc file+              mapM_ addIBC (map (\ (f, h) -> IBCImportHash f h)+                                (mapMaybe id newHashes))+              -- record package info in .ibc+              imps <- allImportDirs+              mapM_ addIBC (map IBCImportDir imps)+              mapM_ (addIBC . IBCImport)+                [ (reexport, realName)+                | ImportInfo { import_reexport = reexport+                             , import_path = realName+                             } <- imports+                ]+              let syntax = defaultSyntax{ syn_namespace = reverse mname,+                                          maxline = toline }+              ist <- getIState+              -- Save the span from parsing the module header, because+              -- an empty program parse might obliterate it.+              let oldSpan = idris_parsedSpan ist+              ds' <- parseProg syntax f file pos -                  -- Parsing done, now process declarations+              case (ds', oldSpan) of+                ([], Just fc) ->+                  -- If no program elements were parsed, we dind't+                  -- get a loaded region in the IBC file. That+                  -- means we need to add it back.+                  do ist <- getIState+                     putIState ist { idris_parsedSpan = oldSpan+                                   , ibc_write = IBCParsedRegion fc :+                                                 ibc_write ist+                                   }+                _ -> return ()+              sendParserHighlighting -                  let ds = namespaces mname ds'-                  logParser 3 (show $ showDecls verbosePPOption ds)-                  i <- getIState-                  logLvl 10 (show (toAlist (idris_implicits i)))-                  logLvl 3 (show (idris_infixes i))-                  -- Now add all the declarations to the context-                  iReport 1 $ "Type checking " ++ f-                  -- we totality check after every Mutual block, so if-                  -- anything is a single definition, wrap it in a-                  -- mutual block on its own-                  elabDecls (toplevelWith f) (map toMutual ds)-                  i <- getIState-                  -- simplify every definition do give the totality checker-                  -- a better chance-                  mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n-                                  ctxt' <--                                    do ctxt <- getContext-                                       tclift $ simplifyCasedef n [] [] (getErasureInfo i) ctxt-                                  setContext ctxt')-                           (map snd (idris_totcheck i))-                  -- build size change graph from simplified definitions-                  iReport 3 $ "Totality checking " ++ f-                  logLvl 1 $ "Totality checking " ++ f-                  i <- getIState-                  mapM_ buildSCG (idris_totcheck i)-                  mapM_ checkDeclTotality (idris_totcheck i)-                  mapM_ verifyTotality (idris_totcheck i)+              -- Parsing done, now process declarations -                  -- Redo totality check for deferred names-                  let deftots = idris_defertotcheck i-                  logLvl 2 $ "Totality checking " ++ show deftots-                  mapM_ (\x -> do tot <- getTotality x-                                  case tot of-                                       Total _ ->-                                         do let opts = case lookupCtxtExact x (idris_flags i) of-                                                          Just os -> os-                                                          Nothing -> []-                                            when (AssertTotal `notElem` opts) $-                                                setTotality x Unchecked-                                       _ -> return ()) (map snd deftots)-                  mapM_ buildSCG deftots-                  mapM_ checkDeclTotality deftots+              let ds = namespaces mname ds'+              logParser 3 (show $ showDecls verbosePPOption ds)+              i <- getIState+              logLvl 10 (show (toAlist (idris_implicits i)))+              logLvl 3 (show (idris_infixes i))+              -- Now add all the declarations to the context+              -- we totality check after every Mutual block, so if+              -- anything is a single definition, wrap it in a+              -- mutual block on its own+              elabDecls (toplevelWith f) (map toMutual ds)+              i <- getIState+              -- simplify every definition do give the totality checker+              -- a better chance+              mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n+                              ctxt' <-+                                do ctxt <- getContext+                                   tclift $ simplifyCasedef n [] [] (getErasureInfo i) ctxt+                              setContext ctxt')+                       (map snd (idris_totcheck i))+              -- build size change graph from simplified definitions+              iReport 3 $ "Totality checking " ++ f+              logLvl 1 $ "Totality checking " ++ f+              i <- getIState+              mapM_ buildSCG (idris_totcheck i)+              mapM_ checkDeclTotality (idris_totcheck i)+              mapM_ verifyTotality (idris_totcheck i) -                  logLvl 1 ("Finished " ++ f)-                  ibcsd <- valIBCSubDir i-                  logLvl  1 $ "Universe checking " ++ f-                  iReport 3 $ "Universe checking " ++ f-                  iucheck-                  let ibc = ibcPathNoFallback ibcsd f-                  i <- getIState-                  addHides (hide_list i)+              -- Redo totality check for deferred names+              let deftots = idris_defertotcheck i+              logLvl 2 $ "Totality checking " ++ show deftots+              mapM_ (\x -> do tot <- getTotality x+                              case tot of+                                   Total _ ->+                                     do let opts = case lookupCtxtExact x (idris_flags i) of+                                                      Just os -> os+                                                      Nothing -> []+                                        when (AssertTotal `notElem` opts) $+                                            setTotality x Unchecked+                                   _ -> return ()) (map snd deftots)+              mapM_ buildSCG deftots+              mapM_ checkDeclTotality deftots -                  -- Save module documentation if applicable-                  i <- getIState-                  case mdocs of-                    Nothing   -> return ()-                    Just docs -> addModDoc syntax mname docs+              logLvl 1 ("Finished " ++ f)+              ibcsd <- valIBCSubDir i+              logLvl  1 $ "Universe checking " ++ f+              iReport 3 $ "Universe checking " ++ f+              iucheck+              i <- getIState+              addHides (hide_list i) +              -- Save module documentation if applicable+              i <- getIState+              case mdocs of+                Nothing   -> return ()+                Just docs -> addModDoc syntax mname docs -                  -- Finally, write an ibc and highlights if checking was successful-                  ok <- noErrors-                  when ok $-                    do idrisCatch (do writeIBC f ibc; clearIBC)-                                  (\c -> return ()) -- failure is harmless-                       hl <- getDumpHighlighting-                       when hl $-                         idrisCatch (writeHighlights f)-                                    (const $ return ()) -- failure is harmless-                  clearHighlights-                  i <- getIState-                  putIState (i { default_total = def_total,-                                 hide_list = emptyContext })-                  return ()++              -- Finally, write an ibc and highlights if checking was successful+              ok <- noErrors+              when ok $+                do idrisCatch (do writeIBC f ibc; clearIBC)+                              (\c -> return ()) -- failure is harmless+                   hl <- getDumpHighlighting+                   when hl $+                     idrisCatch (writeHighlights f)+                                (const $ return ()) -- failure is harmless+              clearHighlights+              i <- getIState+              putIState (i { default_total = def_total,+                             hide_list = emptyContext })+              return ()   where     namespaces :: [String] -> [PDecl] -> [PDecl]     namespaces []     ds = ds

@@ -20,6 +20,7 @@ import Control.Applicative import Control.Arrow (left) import Control.Monad+import qualified Control.Monad.Combinators.Expr as P import Control.Monad.State.Strict import Data.Function (on) import Data.List@@ -27,7 +28,6 @@ import Text.Megaparsec ((<?>)) import qualified Text.Megaparsec as P import qualified Text.Megaparsec.Char as P-import qualified Text.Megaparsec.Expr as P  -- | Allow implicit type declarations allowImp :: SyntaxInfo -> SyntaxInfo@@ -1406,7 +1406,7 @@  -} verbatimStringLiteral :: Parsing m => m String verbatimStringLiteral = token $ do P.try $ string "\"\"\""-                                   str <- P.manyTill P.anyChar $ P.try (string "\"\"\"")+                                   str <- P.manyTill P.anySingle $ P.try (string "\"\"\"")                                    moreQuotes <- P.many $ P.char '"'                                    return $ str ++ moreQuotes 

@@ -36,6 +36,7 @@   , iName   , name   , identifier+  , identifierWithExtraChars   , packageName     -- * Access   , accessibility@@ -199,8 +200,10 @@ {-| Parses a documentation comment  @-  DocComment_t ::=   '|||' ~EOL_t* EOL_t-                 ;+  DocComment_t ::= DocCommentLine (ArgCommentLine DocCommentLine*)* ;++  DocCommentLine ::= '|||' ~EOL_t* EOL_t ;+  ArgCommentLine ::= '|||' '@' ~EOL_t* EOL_t ; @  -} docComment :: IdrisParser (Docstring (), [(Name, Docstring ())])@@ -269,10 +272,10 @@   , "rewrite", "syntax", "then", "total", "using", "where", "with"   ] -identifierOrReserved :: Parsing m => m String-identifierOrReserved = token $ P.try $ do+identifierOrReservedWithExtraChars :: Parsing m => String -> m String+identifierOrReservedWithExtraChars extraChars = token $ P.try $ do   c <- P.satisfy isAlpha <|> P.oneOf "_"-  cs <- P.many (P.satisfy isAlphaNum <|> P.oneOf "_'.")+  cs <- P.many (P.satisfy isAlphaNum <|> P.oneOf extraChars)   return $ c : cs  char :: Parsing m => Char -> m Char@@ -295,13 +298,16 @@   P.notFollowedBy (P.satisfy isAlphaNum <|> P.oneOf "_'.") <?> "end of " ++ name  -- | Parses an identifier as a token-identifier :: Parsing m => m String-identifier = P.try $ do-  ident <- identifierOrReserved+identifierWithExtraChars :: Parsing m => String -> m String+identifierWithExtraChars extraChars = P.try $ do+  ident <- identifierOrReservedWithExtraChars extraChars   when (ident `HS.member` reservedIdentifiers) $ P.unexpected . P.Label . NonEmpty.fromList $ "reserved " ++ ident   when (ident == "_") $ P.unexpected . P.Label . NonEmpty.fromList $ "wildcard"   return ident +identifier :: Parsing m => m String+identifier = identifierWithExtraChars "_'."+ -- | Parses an identifier with possible namespace as a name iName :: Parsing m => [String] -> m Name iName bad = maybeWithNS identifier bad <?> "name"@@ -393,7 +399,7 @@  -- | Gets current indentation indent :: Parsing m => m Int-indent = P.unPos . P.sourceColumn <$> P.getPosition+indent = P.unPos . P.sourceColumn <$> P.getSourcePos  -- | Gets last indentation lastIndent :: (MonadState IState m) => m Int

@@ -17,14 +17,13 @@  import Control.Applicative import Control.Monad+import qualified Control.Monad.Combinators.Expr as P import Control.Monad.State.Strict import Data.Char (isAlpha) import Data.List import Data.List.NonEmpty (fromList) import Text.Megaparsec ((<?>)) import qualified Text.Megaparsec as P-import qualified Text.Megaparsec.Char as P-import qualified Text.Megaparsec.Expr as P  -- | Creates table for fixity declarations to build expression parser -- using pre-build and user-defined operator/fixity declarations

@@ -57,23 +57,34 @@ runparser :: Parser st res -> st -> String -> String -> Either ParseError res runparser p i inputname s =   case P.parse (runWriterT (evalStateT p i)) inputname s of-    Left err -> Left $ ParseError s err+    Left err -> Left $ ParseError err     Right v  -> Right $ fst v  {- * Parse errors -} -data ParseError = ParseError String (P.ParseError (P.Token String) Void)+newtype ParseError = ParseError { unParseError :: P.ParseErrorBundle String Void } +parseError :: ParseError -> P.ParseError String Void+parseError = NonEmpty.head . P.bundleErrors . unParseError++parseErrorPosState :: ParseError -> P.PosState String+parseErrorPosState = P.bundlePosState . unParseError++parseErrorOffset :: ParseError -> Int+parseErrorOffset = P.errorOffset . parseError+ instance Message ParseError where-  messageExtent (ParseError _ err) = sourcePositionFC pos+  messageExtent err = sourcePositionFC pos     where-      (pos NonEmpty.:| _) = P.errorPos err-  messageText (ParseError _ err) = PP.text . init . P.parseErrorTextPretty $ err-  messageSource (ParseError src _) = Just src+      (pos, _) = P.reachOffsetNoLine (parseErrorOffset err) (parseErrorPosState err)+  messageText = PP.text . init . P.parseErrorTextPretty . parseError+  messageSource err = Just sline+    where+      (_, sline, _) = P.reachOffset (parseErrorOffset err) (parseErrorPosState err)  -- | A fully formatted parse error, with caret and bar, etc.-prettyError                    :: ParseError -> String-prettyError (ParseError s err) = P.parseErrorPretty' s err+prettyError :: ParseError -> String+prettyError =  P.errorBundlePretty . unParseError  {- * Mark and restore -} @@ -104,7 +115,7 @@ -- This is useful when the position is needed in a way unrelated to the -- heirarchy of parsers.  Prefer using @withExtent@ and friends. getFC :: Parsing m => m FC-getFC = sourcePositionFC <$> P.getPosition+getFC = sourcePositionFC <$> P.getSourcePos  -- | Add an extent (widen) our current parsing context. addExtent :: MonadWriter FC m => FC -> m ()

@@ -33,7 +33,6 @@ import System.Console.ANSI (Color(..)) import System.FilePath ((</>)) import qualified Text.Megaparsec as P-import qualified Text.Megaparsec.Char as P  parseCmd :: IState -> String -> String -> Either IP.ParseError (Either String Command) parseCmd i inputname = IP.runparser pCmd i inputname . trim@@ -68,7 +67,7 @@   , nameArgCmd ["miss", "missing"] Missing "Show missing clauses"   , (["doc"], NameArg, "Show internal documentation", cmd_doc)   , (["mkdoc"], NamespaceArg, "Generate IdrisDoc for namespace(s) and dependencies"-    , genArg "namespace" (P.many P.anyChar) MakeDoc)+    , genArg "namespace" (P.many P.anySingle) MakeDoc)   , (["apropos"], SeqArgs (OptionalArg PkgArgs) NameArg, " Search names, types, and documentation"     , cmd_apropos)   , (["s", "search"], SeqArgs (OptionalArg PkgArgs) ExprArg@@ -198,7 +197,7 @@     where nop = do P.eof; return (Right NOP)           unrecognized = do               IP.lchar ':'-              cmd <- P.many P.anyChar+              cmd <- P.many P.anySingle               let cmd' = takeWhile (/=' ') cmd               return (Left $ "Unrecognized command: " ++ cmd') @@ -260,7 +259,7 @@ fnNameArg = genArg "functionname" IP.fnName  strArg :: (String -> Command) -> String -> IP.IdrisParser (Either String Command)-strArg = genArg "string" (P.many P.anyChar)+strArg = genArg "string" (P.many P.anySingle)  moduleArg :: (FilePath -> Command) -> String -> IP.IdrisParser (Either String Command) moduleArg = genArg "module" (fmap toPath IP.identifier)@@ -342,7 +341,7 @@  cmd_dynamic :: String -> IP.IdrisParser (Either String Command) cmd_dynamic name = do-    let optArg = do l <- P.many P.anyChar+    let optArg = do l <- P.many P.anySingle                     if (l /= "")                         then return $ Right (DynamicLink l)                         else return $ Right ListDynamic@@ -440,7 +439,7 @@ cmd_loadto :: String -> IP.IdrisParser (Either String Command) cmd_loadto name = do     toline <- fromInteger <$> IP.natural-    f <- P.many P.anyChar+    f <- P.many P.anySingle     return (Right (Load f (Just toline)))  cmd_colour :: String -> IP.IdrisParser (Either String Command)

@@ -0,0 +1,25 @@+#recheck extra-deps next on resolver or cabal file change+resolver: lts-11.4++packages:+  - location: .++extra-deps:+  - network-2.8.0.0@sha256:aae171e6c6028a7791dbe4de5b9d2da398056359e3cc7927465ffa3cdae1aa0b+  - Cabal-2.2.0.1@sha256:2a80d8fb655474f0eaeb20434c47f64f84e6302e55973056f00df8ca050b9683+  - megaparsec-7.0.4+  - parser-combinators-1.0.0+  - zip-archive-0.3.3@sha256:47cf2d66cc8e237f7226837758e1b041e24048ef3820d3d10276c500edb921bf+  - containers-0.5.11.0@sha256:28ad7337057442f75bc689315ab4ec7bdf5e6b2c39668f306672cecd82c02798++flags:+  idris:+    FFI: true+    GMP: true++ghc-options:+  idris: -fwarn-unused-imports -fwarn-unused-binds++nix:+  enable: false+  shell-file: stack-shell.nix

@@ -1,10 +1,15 @@ #recheck extra-deps next on resolver or cabal file change-resolver: lts-11.14--packages:-  - location: .+resolver: lts-13.21 -extra-deps: []+extra-deps:+  - network-2.8.0.0@sha256:aae171e6c6028a7791dbe4de5b9d2da398056359e3cc7927465ffa3cdae1aa0b+  - Cabal-2.2.0.1@sha256:2a80d8fb655474f0eaeb20434c47f64f84e6302e55973056f00df8ca050b9683+  - megaparsec-7.0.4+  - parser-combinators-1.0.0+  - zip-archive-0.3.3@sha256:47cf2d66cc8e237f7226837758e1b041e24048ef3820d3d10276c500edb921bf+  - containers-0.5.11.0@sha256:28ad7337057442f75bc689315ab4ec7bdf5e6b2c39668f306672cecd82c02798+  - tasty-rerun-1.1.14@sha256:ba9c19a281535bea566e1044bc02c36ef17abcb310af4b6a149ec11780c7ce35+  - binary-0.8.7.0@sha256:ae3e6cca723ac55c54bbb3fa771bcf18142bc727afd57818e66d6ee6c8044f12  flags:   idris:

@@ -140,6 +140,8 @@     , (  9, C_CG )     , ( 10, NODE_CG )     , ( 11, NODE_CG )+    , ( 12, NODE_CG )+    , ( 13, C_CG )     ]),   ("folding",         "Folding",     [ (  1, ANY  )]),@@ -182,7 +184,9 @@ --       (  5, ANY  ),       (  6, ANY  ),       (  7, ANY  ),-      (  8, ANY  )]),+      (  8, ANY  ),+--       (  9, ANY  ),+      ( 10, ANY  )]),   ("interpret",      "Interpret",     [ (  1, ANY  ),       (  2, ANY  ),

@@ -11,6 +11,7 @@ import Data.Typeable import Options.Applicative import System.Directory+import System.Environment import System.Exit import System.FilePath ((</>)) import System.Info@@ -103,20 +104,25 @@       normalise (x : xs) = x : normalise xs       normalise [] = [] +checkNode :: IO  ()+checkNode = do+    nodePath   <- findExecutable "node"+    nodejsPath <- findExecutable "nodejs"+    let node = nodePath <|> nodejsPath+    case node of+      Nothing -> do+        putStrLn "For running the test suite against Node, node must be installed."+        exitFailure+      Just _  -> return ()+ main :: IO () main = do-  nodePath   <- findExecutable "node"-  nodejsPath <- findExecutable "nodejs"-  let node = nodePath <|> nodejsPath-  case node of-    Nothing -> do-      putStrLn "For running the test suite against Node, node must be installed."-      exitFailure-    Just _  -> do-      defaultMainWithIngredients ingredients $+    args <- getArgs+    when ("--node" `elem` args) checkNode+    defaultMainWithIngredients ingredients $         askOption $ \(NodeOpt node) ->-          let (codegen, flags) = if node then (JS, ["--codegen", "node"])-                                         else (C , [])-           in-            mkGoldenTests (testFamiliesForCodegen codegen)-                        (flags ++ idrisFlags)+            let (codegen, flags) = if node then (JS, ["--codegen", "node"])+                                           else (C , [])+            in+                mkGoldenTests (testFamiliesForCodegen codegen) (flags ++ idrisFlags)+

@@ -8,7 +8,7 @@     m : C t => t         member of interface         -        The function is Total+        The function is: Total & public export Implementations:     C A         implementation of interface

@@ -1,12 +1,12 @@ T1 : Type     Some documentation     -    The function is Total+    The function is: Total & public export T2 : Type     Some other documentation     -    The function is Total+    The function is: Total & public export T3 : Int     Some provided postulate     -    The function is not yet checked for totality+    The function is: not yet checked for totality & public export

@@ -8,7 +8,7 @@     map : Functor f => (func : a -> b) -> f a -> f b         Apply a function across everything of type 'a' in a parameterised type         -        The function is Total+        The function is: Total & public export Implementations:     Functor (Pair a)     Functor List@@ -33,7 +33,9 @@     docs003.mine : Functor List                  +        The function is: public export Named implementation:     docs003.another : Functor List         More functors!         +        The function is: public export

@@ -7,12 +7,12 @@                  baz : Bool  -- A field baz         -    The function is Total+    The function is: Total & public export Main.Foo.bar : (rec : Foo a) -> Nat     A field bar     -    The function is Total+    The function is: Total & public export Main.Foo.baz : (rec : Foo a) -> Bool     A field baz     -    The function is Total+    The function is: Total & public export

@@ -1,6 +1,7 @@ Data type docs005.Foobar : Type     A foobar with an auto implicit     +    The function is: public export Constructors:     NewFoo : (xs : List String) ->         (ys : List Nat) -> {auto prf : NonEmpty ys} -> Foobar@@ -14,6 +15,7 @@                          (auto implicit) prf : NonEmpty ys  -- The prf             +        The function is: public export docs005.NewFoo : (xs : List String) ->     (ys : List Nat) -> {auto prf : NonEmpty ys} -> Foobar     New Foo@@ -26,4 +28,4 @@                  (auto implicit) prf : NonEmpty ys  -- The prf         -    The function is Total+    The function is: Total & public export

@@ -11,6 +11,6 @@     m : Foo t => t         member of interface         -        The function is Total+        The function is: Total & public export Implementations:     <no implementations>

@@ -4,3 +4,14 @@ foo 1 | 2 | 3 = True foo _ = False +foo2: Int -> Bool+foo2 n with (succ n)+  foo2 n | 1 | 2 = True+  foo2 _ | _ = False++foo3: Int -> Int -> Bool+foo3 n m with (succ n)+  foo3 _ m | 2 with (succ m)+    foo3 _ _ | 2 | 3 | 4 = True+    foo3 _ _ | 2 | _     = False+  foo3 _ _ | _ = True

@@ -5,3 +5,17 @@ When checking left hand side of foo: unexpected patterns outside of "with" block +WithPatsNoWith.idr:9:3-16:+  |+9 |   foo2 n | 1 | 2 = True+  |   ~~~~~~~~~~~~~~+When checking left hand side of with block in WithPatsNoWith.foo2:+unexpected extra "with" patterns++WithPatsNoWith.idr:15:5-24:+   |+15 |     foo3 _ _ | 2 | 3 | 4 = True+   |     ~~~~~~~~~~~~~~~~~~~~+When checking left hand side of with block in with block in WithPatsNoWith.foo3:+unexpected extra "with" patterns+

@@ -0,0 +1,1 @@+Hello?

@@ -0,0 +1,3 @@+l = require("./lib.js");++l.f()

@@ -0,0 +1,14 @@+module Main++export+f : JS_IO ()+f = do+    let res = ()+    let res2 = res+    let res3 = res+    putStrLn' "Hello?"++lib : FFI_Export FFI_JS "" []+lib =+    Fun f "f" $+    End

@@ -0,0 +1,4 @@+#!/usr/bin/env bash+${IDRIS:-idris} $@ ffi012.idr --interface -o lib.js+node ./ffi012+rm -f *.ibc lib.js

@@ -0,0 +1,4 @@+success+confirmed+success+confirmed

@@ -0,0 +1,5 @@+module Main++main : IO ()+main = do b <- fRemove "remove.me"+          putStrLn $ if b then "success" else "failure"

@@ -0,0 +1,17 @@+#!/usr/bin/env bash+echo "test" > remove.me+${IDRIS:-idris} $@ --quiet --port none ffi013.idr -o ffi013+./ffi013+if [ -f "remove.me" ]; then+    echo "still exists"+else +    echo "confirmed"+fi+echo "test2" > remove.me+${IDRIS:-idris} $@ --quiet --port none --nocolour ffi013.idr --exec main+if [ -f "remove.me" ]; then+    echo "still exists"+else +    echo "confirmed"+fi+rm -f ffi013 remove.me *.ibc

@@ -1,10 +1,12 @@ Data type Test.Test : Type     Docs for datatype Test.     +    The function is: public export Constructors:     MkTest : Test                  +        The function is: public export Module Test:     Docs for module Test.     

@@ -3,7 +3,7 @@ Main.main : IO ()     This is a docstring     -    The function is Total+    The function is: Total & public export Main.main is Total Hello, World id : a -> a@@ -27,10 +27,10 @@     is a     docstring     -    The function is Total+    The function is: Total & public export Main.main : IO ()     This is a docstring     -    The function is Total+    The function is: Total & public export Nat2 : Type Invalid filename for compiler output "Test.idr"

@@ -8,7 +8,7 @@     myShow : MyShow a => (x : a) -> String         The shower         -        The function is Total+        The function is: Total & public export Implementation constructor:     MkMyShow : (myShow : a -> String) -> MyShow a         Build a MyShow@@ -17,6 +17,7 @@                          myShow : a -> String  -- The shower             +        The function is: public export Implementations:     MyShow Integer MkMyShow : (myShow : a -> String) -> MyShow a@@ -26,4 +27,4 @@                  myShow : a -> String  -- The shower         -    The function is Total+    The function is: Total & public export

@@ -0,0 +1,12 @@+module Test++interface ListLike a where+  Elem : Type+  fromList : List Elem -> a++data Silly = None | Cons Int Silly++ListLike Silly where+  Elem = Int+  fromList [] = None+  fromList (x :: xs) = Cons x (fromList xs)

@@ -0,0 +1,3 @@+#!/usr/bin/env bash+${IDRIS:-idris} $@ --nocolour --consolewidth 70 interfaces010.idr --check+rm -f interfaces010 *.ibc

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

@@ -2,6 +2,7 @@  sourcedir = src +opts = "--quiet" modules = NumOps         , Test 

@@ -21,8 +21,11 @@         [--codegen TARGET] | [--portable-codegen TARGET] | [--cg-opt ARG] |         [-e|--eval EXPR] | [--execute] | [--exec EXPR] | [-X|--extension EXT] |         [--O3] | [--O2] | [--O1] | [--O0] | [--partial-eval] |-        [--no-partial-eval] | [-O|--level ARG] | [--target TRIPLE] | [--cpu CPU]-        | [--color|--colour] | [--nocolor|--nocolour] | [--consolewidth WIDTH] |-        [--highlight] | [--no-tactic-deprecation-warnings] |+        [--no-partial-eval] |+        [--optimise-nat-like-types|--optimize-nat-like-types] |+        [--no-optimise-nat-like-types|--no-optimize-nat-like-types] |+        [-O|--level ARG] | [--target TRIPLE] | [--cpu CPU] | [--color|--colour]+        | [--nocolor|--nocolour] | [--consolewidth WIDTH] | [--highlight] |+        [--no-tactic-deprecation-warnings] |         [--allow-capitalized-pattern-variables]) [FILES] [-v|--version] )