idris 1.1.1 → 1.2.0

raw patch · 431 files changed

+10565/−9476 lines, 431 filesdep +megaparsecdep +semigroupsdep −parsersdep −transformers-compatdep −trifectadep ~Win32dep ~ansi-terminaldep ~optparse-applicativesetup-changedPVP ok

version bump matches the API change (PVP)

Dependencies added: megaparsec, semigroups

Dependencies removed: parsers, transformers-compat, trifecta

Dependency ranges changed: Win32, ansi-terminal, optparse-applicative, transformers

API changes (from Hackage documentation)

Files

• .github/ISSUE_TEMPLATE.md +9/−0
• .gitignore +1/−0
• CHANGELOG.md +128/−0
• CONTRIBUTING.md +15/−0
• CONTRIBUTORS +9/−0
• Setup.hs +11/−1
• appveyor.yml +7/−6
• benchmarks/fasta/fasta.idr +0/−4
• codegen/idris-codegen-c/Main.hs +0/−3
• codegen/idris-codegen-javascript/Main.hs +0/−3
• codegen/idris-codegen-node/Main.hs +9/−4
• docs/conf.py +7/−6
• docs/effects/state.rst +1/−1
• docs/faq/faq.rst +7/−2
• docs/faq/index.rst +0/−19
• 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/inductive.rst +2/−0
• docs/reference/ffi.rst +123/−2
• docs/reference/ide-protocol.rst +1/−1
• docs/reference/misc.rst +0/−107
• docs/reference/packages.rst +4/−1
• docs/reference/syntax-guide.rst +2/−3
• docs/st/state.rst +16/−18
• docs/tutorial/index.rst +2/−1
• docs/tutorial/interfaces.rst +6/−6
• docs/tutorial/miscellany.rst +9/−1
• docs/tutorial/modules.rst +0/−4
• docs/tutorial/starting.rst +1/−1
• docs/tutorial/views.rst +42/−15
• idris-tutorial.pdf binary
• idris.cabal +18/−13
• libs/base/Control/Category.idr +1/−1
• libs/base/Control/Monad/State.idr +4/−0
• libs/base/Data/Buffer.idr +34/−2
• libs/base/Data/Complex.idr +5/−10
• libs/base/Data/IORef.idr +54/−0
• libs/base/Data/List.idr +24/−9
• libs/base/Data/Morphisms.idr +12/−0
• libs/base/Data/Primitives/Views.idr +19/−15
• libs/base/Data/Vect.idr +18/−0
• libs/base/Language/Reflection/Utils.idr +8/−1
• libs/base/System.idr +1/−0
• libs/base/base.ipkg +43/−37
• libs/contrib/CFFI/Memory.idr +3/−2
• libs/contrib/CFFI/Types.idr +5/−5
• libs/contrib/Control/Delayed.idr +26/−0
• libs/contrib/Control/Monad/Syntax.idr +18/−0
• libs/contrib/Control/ST.idr +6/−11
• libs/contrib/Control/ST/File.idr +247/−0
• libs/contrib/Control/ST/Random.idr +42/−0
• libs/contrib/Data/Bool/Extra.idr +32/−0
• libs/contrib/Data/Combinators.idr +39/−0
• libs/contrib/Data/Combinators/Applicative.idr +27/−0
• libs/contrib/Data/Combinators/Arrow.idr +15/−0
• libs/contrib/Data/Fuel.idr +18/−0
• libs/contrib/Data/IOArray.idr +47/−0
• libs/contrib/Data/List/Group.idr +24/−0
• libs/contrib/Data/List/Permutations.idr +10/−0
• libs/contrib/Data/Matrix/Numeric.idr +3/−1
• libs/contrib/Data/Nat/Parity.idr +16/−0
• libs/contrib/Data/Pairs/Implicit.idr +13/−0
• libs/contrib/Data/Stream/Extra.idr +10/−0
• libs/contrib/Data/String.idr +0/−31
• libs/contrib/Data/String/Extra.idr +88/−0
• libs/contrib/Data/ZZ.idr +5/−3
• libs/contrib/Interfaces/Correlative.idr +63/−0
• libs/contrib/Language/JSON.idr +14/−0
• libs/contrib/Language/JSON/Data.idr +98/−0
• libs/contrib/Language/JSON/Lexer.idr +40/−0
• libs/contrib/Language/JSON/Parser.idr +71/−0
• libs/contrib/Language/JSON/String.idr +16/−0
• libs/contrib/Language/JSON/String/Lexer.idr +38/−0
• libs/contrib/Language/JSON/String/Parser.idr +25/−0
• libs/contrib/Language/JSON/String/Tokens.idr +60/−0
• libs/contrib/Language/JSON/Tokens.idr +72/−0
• libs/contrib/Network/Socket.idr +1/−5
• libs/contrib/Network/Socket/Raw.idr +0/−3
• libs/contrib/Test/Unit.idr +14/−0
• libs/contrib/Test/Unit/Assertions.idr +37/−0
• libs/contrib/Test/Unit/Display.idr +27/−0
• libs/contrib/Test/Unit/Generic.idr +43/−0
• libs/contrib/Test/Unit/Runners.idr +36/−0
• libs/contrib/Text/Lexer.idr +250/−198
• libs/contrib/Text/Lexer/Core.idr +193/−0
• libs/contrib/Text/Literate.idr +155/−0
• libs/contrib/Text/Parser.idr +194/−238
• libs/contrib/Text/Parser/Core.idr +265/−0
• libs/contrib/Text/PrettyPrint/WL/Core.idr +5/−4
• libs/contrib/Text/Quantity.idr +38/−0
• libs/contrib/Text/Token.idr +38/−0
• libs/contrib/contrib.ipkg +89/−28
• libs/effects/Effect/Logging/Level.idr +9/−9
• libs/effects/Effects.idr +0/−7
• libs/effects/effects.ipkg +12/−10
• libs/oldeffects/Effect/Default.idr +0/−44
• libs/oldeffects/Effect/Exception.idr +0/−41
• libs/oldeffects/Effect/File.idr +0/−128
• libs/oldeffects/Effect/Memory.idr +0/−175
• libs/oldeffects/Effect/Monad.idr +0/−21
• libs/oldeffects/Effect/Random.idr +0/−47
• libs/oldeffects/Effect/Select.idr +0/−23
• libs/oldeffects/Effect/State.idr +0/−40
• libs/oldeffects/Effect/StdIO.idr +0/−60
• libs/oldeffects/Effect/System.idr +0/−43
• libs/oldeffects/Effects.idr +0/−333
• libs/oldeffects/Makefile +0/−22
• libs/oldeffects/effects.ipkg +0/−9
• libs/prelude/Builtins.idr +6/−19
• libs/prelude/Decidable/Equality.idr +12/−6
• libs/prelude/IO.idr +3/−2
• libs/prelude/Language/Reflection.idr +1/−9
• libs/prelude/Language/Reflection/Elab.idr +0/−6
• libs/prelude/Prelude.idr +3/−4
• libs/prelude/Prelude/Applicative.idr +4/−4
• libs/prelude/Prelude/Basics.idr +1/−2
• libs/prelude/Prelude/Bits.idr +0/−25
• libs/prelude/Prelude/Bool.idr +2/−1
• libs/prelude/Prelude/Chars.idr +5/−0
• libs/prelude/Prelude/Doubles.idr +1/−1
• libs/prelude/Prelude/File.idr +56/−31
• libs/prelude/Prelude/Functor.idr +3/−3
• libs/prelude/Prelude/Interfaces.idr +21/−9
• libs/prelude/Prelude/List.idr +14/−14
• libs/prelude/Prelude/Maybe.idr +6/−0
• libs/prelude/Prelude/Monad.idr +3/−8
• libs/prelude/Prelude/Nat.idr +29/−2
• libs/prelude/Prelude/Pairs.idr +0/−8
• libs/prelude/prelude.ipkg +36/−11
• libs/pruviloj/Pruviloj/Core.idr +19/−0
• libs/pruviloj/Pruviloj/Derive/Eliminators.idr +2/−2
• libs/pruviloj/Pruviloj/Disjoint.idr +65/−25
• libs/pruviloj/pruviloj.ipkg +7/−1
• main/Main.hs +1/−6
• man/idris.1 +1/−1
• rts/Makefile +3/−4
• rts/idris_buffer.c +42/−0
• rts/idris_buffer.h +4/−0
• rts/idris_gc.c +22/−4
• rts/idris_gmp.c +6/−6
• rts/idris_gmp.h +2/−1
• rts/idris_net.c +37/−8
• rts/idris_net.h +13/−0
• rts/idris_rts.c +50/−2
• rts/idris_rts.h +32/−13
• rts/idris_stdfgn.c +49/−4
• rts/idris_stdfgn.h +11/−2
• rts/idris_utf8.c +1/−1
• rts/windows/idris_net.c +0/−200
• samples/ST/Login.idr +1/−1
• samples/tutorial/BTreeMod.idr +5/−5
• src/IRTS/BCImp.hs +0/−23
• src/IRTS/Bytecode.hs +1/−2
• src/IRTS/CodegenC.hs +42/−45
• src/IRTS/CodegenCommon.hs +1/−1
• src/IRTS/CodegenJavaScript.hs +16/−7
• src/IRTS/Compiler.hs +35/−36
• src/IRTS/Defunctionalise.hs +23/−75
• src/IRTS/DumpBC.hs +1/−2
• src/IRTS/Exports.hs +1/−1
• src/IRTS/Inliner.hs +1/−1
• src/IRTS/JavaScript/AST.hs +1/−1
• src/IRTS/JavaScript/Codegen.hs +80/−61
• src/IRTS/JavaScript/LangTransforms.hs +3/−13
• src/IRTS/JavaScript/Name.hs +1/−4
• src/IRTS/JavaScript/PrimOp.hs +6/−7
• src/IRTS/JavaScript/Specialize.hs +1/−15
• src/IRTS/Lang.hs +114/−54
• src/IRTS/LangOpts.hs +262/−51
• src/IRTS/Portable.hs +3/−4
• src/IRTS/Simplified.hs +4/−9
• src/IRTS/System.hs +1/−1
• src/Idris/ASTUtils.hs +1/−2
• src/Idris/AbsSyntax.hs +38/−53
• src/Idris/AbsSyntaxTree.hs +45/−58
• src/Idris/Apropos.hs +3/−9
• src/Idris/CaseSplit.hs +1/−1
• src/Idris/Chaser.hs +23/−22
• src/Idris/CmdOptions.hs +2/−5
• src/Idris/Colours.hs +1/−1
• src/Idris/Completion.hs +13/−12
• src/Idris/Core/Binary.hs +16/−339
• src/Idris/Core/CaseTree.hs +58/−66
• src/Idris/Core/Constraints.hs +3/−5
• src/Idris/Core/DeepSeq.hs +1/−1
• src/Idris/Core/Elaborate.hs +9/−27
• src/Idris/Core/Evaluate.hs +24/−56
• src/Idris/Core/Execute.hs +8/−44
• src/Idris/Core/ProofState.hs +37/−82
• src/Idris/Core/ProofTerm.hs +34/−39
• src/Idris/Core/TT.hs +50/−84
• src/Idris/Core/Typecheck.hs +30/−56
• src/Idris/Core/Unify.hs +6/−95
• src/Idris/Core/WHNF.hs +3/−6
• src/Idris/Coverage.hs +1/−11
• src/Idris/DSL.hs +15/−17
• src/Idris/DataOpts.hs +2/−8
• src/Idris/DeepSeq.hs +1/−2
• src/Idris/Delaborate.hs +10/−18
• src/Idris/Directives.hs +1/−2
• src/Idris/Docs.hs +1/−5
• src/Idris/Docstrings.hs +1/−1
• src/Idris/Elab/AsPat.hs +22/−11
• src/Idris/Elab/Clause.hs +20/−62
• src/Idris/Elab/Data.hs +5/−43
• src/Idris/Elab/Implementation.hs +5/−31
• src/Idris/Elab/Interface.hs +14/−48
• src/Idris/Elab/Provider.hs +1/−28
• src/Idris/Elab/Quasiquote.hs +6/−6
• src/Idris/Elab/Record.hs +2/−41
• src/Idris/Elab/Rewrite.hs +7/−9
• src/Idris/Elab/RunElab.hs +2/−4
• src/Idris/Elab/Term.hs +54/−89
• src/Idris/Elab/Transform.hs +2/−31
• src/Idris/Elab/Type.hs +2/−47
• src/Idris/Elab/Utils.hs +75/−27
• src/Idris/Elab/Value.hs +3/−31
• src/Idris/ElabDecls.hs +10/−34
• src/Idris/Erasure.hs +4/−11
• src/Idris/ErrReverse.hs +1/−13
• src/Idris/Error.hs +7/−12
• src/Idris/Help.hs +1/−1
• src/Idris/IBC.hs +1041/−2563
• src/Idris/IdeMode.hs +24/−26
• src/Idris/IdrisDoc.hs +13/−21
• src/Idris/Imports.hs +42/−7
• src/Idris/Info.hs +1/−2
• src/Idris/Inliner.hs +2/−2
• src/Idris/Interactive.hs +3/−5
• src/Idris/Main.hs +20/−21
• src/Idris/ModeCommon.hs +25/−26
• src/Idris/Options.hs +10/−2
• src/Idris/Output.hs +154/−14
• src/Idris/Package.hs +32/−25
• src/Idris/Package/Common.hs +4/−3
• src/Idris/Package/Parser.hs +57/−170
• src/Idris/Parser.hs +377/−454
• src/Idris/Parser/Data.hs +73/−101
• src/Idris/Parser/Expr.hs +298/−373
• src/Idris/Parser/Helpers.hs +214/−374
• src/Idris/Parser/Ops.hs +123/−82
• src/Idris/Parser/Stack.hs +136/−0
• src/Idris/PartialEval.hs +8/−15
• src/Idris/Primitives.hs +16/−50
• src/Idris/ProofSearch.hs +6/−22
• src/Idris/Prover.hs +35/−36
• src/Idris/Providers.hs +1/−3
• src/Idris/REPL.hs +55/−52
• src/Idris/REPL/Browse.hs +1/−1
• src/Idris/REPL/Commands.hs +4/−2
• src/Idris/REPL/Parser.hs +167/−164
• src/Idris/Reflection.hs +20/−8
• src/Idris/Termination.hs +15/−22
• src/Idris/Transforms.hs +1/−4
• src/Idris/TypeSearch.hs +7/−10
• src/Idris/Unlit.hs +1/−1
• src/Idris/WhoCalls.hs +3/−3
• src/Util/DynamicLinker.hs +17/−10
• src/Util/Net.hs +1/−1
• src/Util/Pretty.hs +1/−1
• src/Util/ScreenSize.hs +1/−1
• src/Util/System.hs +1/−1
• stack-shell.nix +5/−15
• stack.yaml +5/−4
• test/README.md +1/−0
• test/TestData.hs +46/−23
• test/TestRun.hs +0/−2
• test/basic002/expected +10/−2
• test/basic006/expected +6/−1
• test/basic009/expected +18/−3
• test/basic013/basic013.idr +2/−0
• test/basic013/expected +2/−0
• test/basic016/expected +1/−1
• test/basic017/expected +6/−1
• test/basic018/expected +16/−3
• test/basic020/basic020.idr +42/−0
• test/basic020/expected +1/−0
• test/basic020/run +4/−0
• test/basic021/basic021.idr +13/−0
• test/basic021/basic021_2.idr +13/−0
• test/basic021/expected +2/−0
• test/basic021/run +6/−0
• test/basic022/basic022.idr +13/−0
• test/basic022/expected +1/−0
• test/basic022/run +4/−0
• test/basic023/expected +10/−0
• test/basic023/run +4/−0
• test/basic023/sections.idr +34/−0
• test/basic024/basic024.idr +51/−0
• test/basic024/expected +76/−0
• test/basic024/input +46/−0
• test/basic024/run +8/−0
• test/basic025/basic025.idr +28/−0
• test/basic025/expected +12/−0
• test/basic025/input +7/−0
• test/basic025/run +7/−0
• test/bignum002/bignum002.idr +10/−1
• test/bignum002/expected +7/−0
• test/buffer002/buffer002.idr +27/−0
• test/buffer002/expected +10/−0
• test/buffer002/run +4/−0
• test/contrib001/contrib001.idr +14/−0
• test/contrib001/expected +12/−0
• test/contrib001/run +4/−0
• test/directives001/expected +36/−6
• test/directives002/expected +5/−1
• test/directives003/directives003.idr +11/−0
• test/directives003/expected +6/−0
• test/directives003/run +13/−0
• test/effects003/expected +5/−1
• test/error001/expected +6/−1
• test/error003/expected +6/−1
• test/error004/expected +10/−2
• test/error005/expected +30/−5
• test/error006/expected +6/−1
• test/error007/expected +5/−1
• test/error008/expected +12/−2
• test/ffi002/expected +6/−1
• test/ffi007/expected +1/−0
• test/ffi007/ffi007.h +2/−0
• test/ffi007/ffi007.idr +5/−0
• test/ffi008/ffi008.c +12/−1
• test/ffi008/ffi008.h +2/−0
• test/ffi008/ffi008.idr +10/−0
• test/ffi011/expected +2/−0
• test/ffi011/ffi011 +7/−0
• test/ffi011/ffi011.idr +27/−0
• test/ffi011/run +4/−0
• test/interactive010/expected +15/−11
• test/interactive017/run +0/−0
• test/interactive018/Imported1.idr +10/−0
• test/interactive018/Imported2.idr +8/−0
• test/interactive018/Public1.idr +10/−0
• test/interactive018/Public2.idr +8/−0
• test/interactive018/Top.idr +11/−0
• test/interactive018/expected +20/−0
• test/interactive018/input +20/−0
• test/interactive018/run +3/−0
• test/interfaces008/expected +6/−0
• test/interfaces008/interfaces008.idr +20/−0
• test/interfaces008/run +3/−0
• test/interfaces009/expected +0/−0
• test/interfaces009/interfaces009.idr +24/−0
• test/interfaces009/run +3/−0
• test/layout001/expected +78/−72
• test/literate001/expected +6/−1
• test/meta002/expected +15/−3
• test/meta003/expected +5/−1
• test/meta004/expected +5/−1
• test/pkg001/test-pkg.ipkg +1/−1
• test/pkg004/expected +6/−5
• test/pkg004/test.ipkg +1/−1
• test/primitives003/expected +4/−0
• test/primitives003/test038.idr +14/−10
• test/proof001/expected +10/−2
• test/proof002/expected +20/−4
• test/proof003/expected +30/−6
• test/proof007/expected +5/−1
• test/proof008/expected +5/−1
• test/proof011/expected +12/−2
• test/pruviloj001/pruviloj001.idr +13/−0
• test/quasiquote003/expected +6/−1
• test/quasiquote004/expected +20/−4
• test/quasiquote006/expected +16/−4
• test/reg017/expected +10/−2
• test/reg027/expected +6/−1
• test/regression002/expected +270/−67
• test/sourceLocation001/expected +24/−8
• test/st001/expected +8/−0
• test/st001/run +6/−0
• test/st001/test001.idr +66/−0
• test/st001/testFile +2/−0
• test/st002/expected +8/−0
• test/st002/run +6/−0
• test/st002/test002.idr +66/−0
• test/st002/testFile +2/−0
• test/st003/expected +8/−0
• test/st003/run +6/−0
• test/st003/test003.idr +25/−0
• test/st003/testFile +2/−0
• test/st004/expected +6/−0
• test/st004/run +6/−0
• test/st004/test004.idr +24/−0
• test/st005/expected +6/−0
• test/st005/run +7/−0
• test/st005/test005.idr +33/−0
• test/st006/expected +5/−0
• test/st006/run +6/−0
• test/st006/test006.idr +37/−0
• test/st007/expected +6/−0
• test/st007/run +6/−0
• test/st007/test007.idr +24/−0
• test/sugar004/expected +1/−0
• test/sugar004/run +1/−0
• test/sugar004/sugar004.idr +12/−1
• test/syntax001/expected +12/−2
• test/totality001/expected +18/−3
• test/totality002/expected +16/−3
• test/totality003/expected +5/−1
• test/totality004/expected +11/−2
• test/totality006/expected +17/−3
• test/totality007/expected +6/−2
• test/totality008/expected +6/−1
• test/totality009/expected +60/−10
• test/totality010/expected +12/−2
• test/totality011/expected +5/−1
• test/totality012/expected +10/−2
• test/totality013/expected +11/−2
• test/totality014/expected +9/−4
• test/totality015/expected +17/−3
• test/totality016/expected +54/−9
• test/totality017/expected +36/−6
• test/totality018/expected +6/−1
• test/totality019/expected +12/−2
• test/totality020/expected +12/−2
• test/totality021/expected +26/−5
• test/totality022/expected +6/−1
• test/totality023/expected +5/−1
• test/totality024/expected +1/−0
• test/totality024/run +3/−0
• test/totality024/totality023.idr +7/−0
• test/tutorial002/expected +15/−3
• test/tutorial004/expected +10/−2
• test/tutorial006/expected +10/−2
• test/unique004/expected +59/−10
• test/universes001/expected +10/−5
• test/universes002/expected +10/−5
• test/views001/views001.idr +1/−1
• test/views001/views001a.idr +1/−1
• test/views002/views002.idr +1/−1

@@ -0,0 +1,9 @@+Please attach complete source files that exhibit the issue in addition+to quoting from them here.++# Steps to Reproduce++# Expected Behavior++# Observed Behavior+

@@ -1,5 +1,6 @@ # Build artefacts dist+dist-newstyle *.ibc *.o *.a

@@ -1,3 +1,131 @@+# New in 1.2.0++## Language updates+++ In `@`-patterns such as `x@p`, `x` is now in scope on the right-hand side+  of any definitions in `where` clauses, provided the left-hand side of the+  definition does not shadow it.++ The `LinearTypes` language extension has been revised. It implements the+  rules from Bob Atkey's draft "The Syntax and Semantics of Quantitative+  Type Theory" and now works with holes and case expressions.++ Backticked operators can appear in sections, e.g. ``(`LTE` 42)`` or+  ``(1 `plus`)``.++ Backticked operators can have their precendence and associativity set like+  other operators, e.g. ``infixr 8 `cons` ``.  Backticked operators with+  undeclared fixity are treated as non-associative with precedence lower+  than all declared operators.++ Allow non-injective implementations if explicitly named, e.g.,+  ```idris+  LTB : Nat -> Type+  LTB b = DPair Nat (\ n  => LT n b)++  implementation [uninhabltb] Uninhabited (LTB Z) where+    uninhabited (MkDPair n prf) = absurd prf+  ```+  It is possible to use `using implementation uninhabltb` to add the+  implementation to the automated resolution, but if it fails to find the+  instance due to non-injectivity, one must pass it explicitly to target+  function, i.e. `absurd @{uninhabltb}`.++ Verbatim strings now support trailing quote characters. All quote characters+  until the final three are considered part of the string. Now a string such as+  `""""hello""""` will parse, and is equivalent to `"\"hello\""`.++ C FFI now supports pasting in any expression by prefixing it with '#', e.g.+  ```idris+  intMax : IO Int+  intMax = foreign FFI_C "#INT_MAX" (IO Int) +  ```++ The deprecated keywords `%assert_total`, `abstract`, and `[static]` have+  been removed as well as the use of "public" instead of "public export" to+  expose a symbol.++ The syntax for pattern-match alternatives now works for `let` statements in+  `do` blocks in addition to `let` expressions and `<-` statements, e.g.+  ```idris+    do …+       let Just x = expr | Nothing => empty+       …+  ```+  This means that a `with`-application (using `|`) cannot be used in that+  position anymore.++## Library Updates+++ Removed `oldeffects` library from `libs` folder, use `effects` or `Control.ST` instead.++ Added `Text.Literate`, a module for working with literate source files.++ Added `Data.IORef`, for working with mutable references in `IO` and `JS_IO`.++ Added `discriminate` and `construct` tactics to Pruviloj.++ Added `IsSucc` type to `Prelude`, which proves that a `Nat` is a successor.++ Added `Data.IOArray`, containing primitives for mutable arrays.++ Added `Language.JSON`, for total serialization/deserialization of JSON data.++ Reworked operator fixity for many operators.+  * Changed `&&` and `||` to be right-associative. Increased precedence of `&&`+    to be higher than that of `||`.+  * Removed associativity from Boolean comparison operators `==`, `/=`, `<`, `<=`,+    `>`, and `>=`. Increased precedence of `/=` and `==` to match the others.+  * Made `<|>`, `<$>`, and `.` right-associative.+  * Swapped precedence of `<|>` and `<*>` (and its related operators, `<*` and+    `*>`). Now `<|>` has a lower precedence.+  * Lowered the precedence of `>>=` to be below that of `<|>`.++ Added some useful string manipulation functions to `Data.String.Extra`.++ Added `Control.Delayed`, a module for conditionally making a type `Inf` or `Lazy`.++ Added `Data.Fuel`, which implements the `Fuel` data type and the partial `forever` function.++ Added `Data.Bool.Extra`, a module with properties of boolean operations.++ Moved core of `Text.Lexer` to `Text.Lexer.Core`. Added several new combinators+  and lexers to `Text.Lexer`.++ Moved core of `Text.Parser` to `Text.Parser.Core`. Added several new combinators+  to `Text.Parser`. Made the following changes.+  * Flipped argument order of `parse`.+  * Renamed `optional` to `option` and flip argument order.+  * Renamed `maybe` to `optional`.+  * Generalised many combinators to use an unknown `commit` flag where possible.++ `Prelude.Doubles.atan2` is now implemented as a primitive instead of+  being coded in Idris.++ Added `Test.Unit` to `contrib` for simple unit testing.++ Removed several deprecated items from the libraries shipped with Idris.++ Moved `abs` from the `Neg` interface into its own `Abs` interface.  `Nat`+  implements `Abs` with `abs = id`.++ Added `Control.ST.File`, an ST based implementation of the same behaviour +  implemented by `Effect.File` in the effects package.++## Tool Updates+++ Private functions are no longer visible in the REPL except for modules+  that are explicitly loaded.++ The --interface option now creates CommonJS modules on the node backend.++ The C backend now pass arguments to the C compiler in the same order+  as they were given in the source files.++ Backslash, braces and percent symbols are now correctly pretty printed+  in LaTeX.++ Errors and warnings now consistently have the following format:+  ```idris+  reg068.idr:1:6-8:+    |+  1 | data nat : Type where --error+    |      ~~~+  Main.nat has a name which may be implicitly bound.+  This is likely to lead to problems!+  ```+  The code is highlighted when highlighting information is available.  How+  much highlighting information is available depends on where the error+  occurred.++ The parser provider has been switched from Trifecta to Megaparsec.  This+  could possibly cause some subtle deviations in parsing from previous+  versions of Idris.++ Many more errors now report beginning *and* ending position (which may be+  on different lines), instead of just a single point.  The format is+  `Foo.idr:9:7-15:` if ending column is on the same line or+  `Foo.idr:9:7-10:15:` if the ending column is on a different line.++ Error messages were changed so that the last column is inclusive, e.g.+  `Foo.idr:9:7-15:` includes column 15.  Previously the error would have read+  `Foo.idr:9:7-16:`.++## Packaging Updates+++ Package names now only accept a restrictive charset of letters, numbers and the `-_` characters.+  Package names are also case insensitive.++ When building makefiles for the FFI, the environment variables+  `IDRIS_INCLUDES` and `IDRIS_LDFLAGS` are now set with the correct C+  flags.+ # New in 1.1.1  + Erasure analysis is now faster thanks to a bit smarter constraint solving.

@@ -20,6 +20,21 @@ Before you report an issue, or wish to add cool functionality please try and check to see if there are existing [issues](https://github.com/idris-lang/Idris-dev/issues) and [pull requests](https://github.com/idris-lang/Idris-dev/pulls). We do not want you wasting your time, duplicating somebody's work! +### Template+Try as closely as possible to describe the issue, ensuring that it has sections that match the following headings:+> \# Steps to Reproduce+>+> \# Expected Behavior+> +> \# Observed Behavior+> +>++In addition, please attach complete source files that exhibit the issue to quoting from them in the issue.++### Feature Requests+We would be delighted to receive feature requests only if they are feasible to implement and the author is willing to implement the suggested features themself. The current Idris developer team consists mostly of volunteers, and so it is unfortunately hard to accommodate implementing nice-to-have ideas that are not essential for core language development.+ ## The Campsite Rule  We try to follow the **campsite rule**: leave the code base in better condition than you found it.

@@ -8,6 +8,7 @@ Ahmad Salim Al-Sibahi Aistis Raulinaitis Alex Feldman-Crough+Alex S. Queiroz e Silva Alexander Berntsen Alexander Shabalin Alyssa Carter@@ -33,6 +34,7 @@ Brian Koropoff Brian McKenna Bryn Keller+Caleb Case Calvin Beck Carsten König Carter Charbonneau@@ -106,6 +108,7 @@ Jan Doms Jan Stolarek Jason Dagit+Jason Felice Jason Gross Jean-Remi Desjardins Jeff Hemphill@@ -119,8 +122,10 @@ John Dobronszki John Wiegley Jon Atack+Jonas De Vuyst Jonas Westerlund Jonathan Sterling+Joomy Korkut Joseph Huang Josh Vera JP Smith@@ -151,6 +156,7 @@ Michael Hensler Michael Maloney Michael McGirr+Michael Morgan Michael Thompson Michael Weiss Miikka Koskinen@@ -176,6 +182,7 @@ Robert Clipsham Robert Edström Ross Meikleham+Rui Barreiro Ryan Scott Sam Elliott Sam T@@ -197,9 +204,11 @@ suhorng Sune Alkærsig Sven Koschnicke+Taran Lynn tdidriksen Tenor Biel Thomas Cooper+Thomas Scholtes Tim Dysinger Tim McGilchrist Timo Petteri Sinnemäki

@@ -26,6 +26,11 @@ import qualified System.FilePath.Posix as Px import System.Process +#if (MIN_VERSION_Cabal(2,0,0))+import Distribution.Types.UnqualComponentName+#endif++ -- After Idris is built, we need to check and install the prelude and other libs  -- -----------------------------------------------------------------------------@@ -228,11 +233,16 @@       let buildinfo = (emptyBuildInfo { cppOptions = ["-DVERSION="++hash] }) :: BuildInfo       return (Just buildinfo, []) ++#if !(MIN_VERSION_Cabal(2,0,0))+mkUnqualComponentName = id+#endif+ idrisPreBuild args flags = do #ifdef mingw32_HOST_OS         createDirectoryIfMissingVerbose verbosity True dir         windres verbosity ["icons/idris_icon.rc","-o", dir++"/idris_icon.o"]-        return (Nothing, [("idris", emptyBuildInfo { ldOptions = [dir ++ "/idris_icon.o"] })])+        return (Nothing, [(mkUnqualComponentName "idris", emptyBuildInfo { ldOptions = [dir ++ "/idris_icon.o"] })])      where         verbosity = S.fromFlag $ S.buildVerbosity flags         dir = S.fromFlagOrDefault "dist" $ S.buildDistPref flags

@@ -5,13 +5,13 @@      mkdir C:\ghc -    Invoke-WebRequest "http://downloads.haskell.org/~ghc/7.10.3/ghc-7.10.3-x86_64-unknown-mingw32.tar.xz" -OutFile C:\ghc\ghc.tar.xz -UserAgent "Curl"-    +    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"+     7z x C:\ghc\ghc.tar.xz -oC:\ghc-    +     7z x C:\ghc\ghc.tar -oC:\ghc -    $env:PATH="$env:PATH;c:\ghc\ghc-7.10.3\bin;$HOME\AppData\Roaming\cabal\bin"+    $env:PATH="$env:PATH;c:\ghc\ghc-8.2.1\bin;$HOME\AppData\Roaming\cabal\bin"      cabal update @@ -21,6 +21,7 @@   MSYSTEM: MINGW64   MSYS2_PATH_TYPE: inherit build_script:-- ps: c:\msys64\usr\bin\bash -l -c "cd $env:current_posix && cabal install -fffi -j4 --enable-tests"+- ps: >-+    c:\msys64\usr\bin\bash -l -c "cd $env:current_posix && cabal install -fffi --enable-tests 2>&1" test_script:-- ps: c:\msys64\usr\bin\bash -l -c "cd $env:current_posix && make test_c"+- ps: c:\msys64\usr\bin\bash -l -c "cd $env:current_posix && make test_c 2>&1"

@@ -38,10 +38,6 @@ replicate 0 c = "" replicate n c = singleton c <+> replicate (n-1) c -scanl : (f : acc -> a -> acc) -> acc -> List a -> List acc-scanl f q ls = q :: (case ls of-                        []    => []-                        x::xs => scanl f (f q x) xs)  accum : (Char,Double) -> (Char,Double) -> (Char,Double) accum (_,p) (c,q) = (c,p+q)

@@ -1,7 +1,6 @@ module Main where  import Idris.AbsSyntax-import Idris.Core.TT import Idris.ElabDecls import Idris.Main import Idris.Options@@ -9,8 +8,6 @@ import IRTS.Compiler  import Util.System--import Paths_idris  import Control.Monad import System.Environment

@@ -1,14 +1,11 @@ module Main where  import Idris.AbsSyntax-import Idris.Core.TT import Idris.ElabDecls import Idris.Main import Idris.Options import IRTS.CodegenJavaScript import IRTS.Compiler--import Paths_idris  import System.Environment import System.Exit

@@ -1,7 +1,6 @@ module Main where  import Idris.AbsSyntax-import Idris.Core.TT import Idris.ElabDecls import Idris.Main import Idris.Options@@ -10,10 +9,13 @@  import Paths_idris +import Control.Monad+ import System.Environment import System.Exit  data Opts = Opts { inputs :: [FilePath]+                 , interface :: Bool                  , output :: FilePath                  } @@ -23,17 +25,20 @@  getOpts :: IO Opts getOpts = do xs <- getArgs-             return $ process (Opts [] "main.js") xs+             return $ process (Opts [] False "main.js") xs   where     process opts ("-o":o:xs) = process (opts { output = o }) xs+    process opts ("--interface":xs) = process (opts { interface = True }) xs     process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs     process opts [] = opts  jsMain :: Opts -> Idris () jsMain opts = do elabPrims                  loadInputs (inputs opts) Nothing-                 mainProg <- elabMain-                 ir <- compile (Via IBCFormat "node") (output opts) (Just mainProg)+                 mainProg <- if interface opts+                                then return Nothing+                                else liftM Just elabMain+                 ir <- compile (Via IBCFormat "node") (output opts) mainProg                  runIO $ codegenNode ir  main :: IO ()

@@ -59,9 +59,9 @@ # built documents. # # The short X.Y version.-version = '1.0'+version = '1.2' # The full version, including alpha/beta/rc tags.-release = '1.0'+release = '1.2.0'  # The language for content autogenerated by Sphinx. Refer to documentation # for a list of supported languages.@@ -222,7 +222,7 @@     \begin{center}         \includegraphics[width=0.25\textwidth]{idris-512x512.png}\par         \vspace{1cm}-        {\huge\sffamily\bfseries Documentation for the Idris Language\par}+        {\huge\sffamily\bfseries \makeatletter\@title\makeatother\par}         \vspace{1cm}         {\Large Version \version\par}     \end{center}@@ -284,8 +284,8 @@ \definecolor{VerbatimBorderColor}{rgb}{1,1,1} ''', -'maketitle': latex_title_page-+'maketitle': latex_title_page,+'tableofcontents': "\\tableofcontents" # Latex figure (float) alignment #'figure_align': 'htbp', }@@ -294,7 +294,8 @@ # (source start file, target name, title, #  author, documentclass [howto, manual, or own class]). latex_documents = [-  ('index',  'idris.tex',  u'Documentation for the Idris Language',    u'The Idris Community', 'report')+  ('index',  'idris-documentation-complete.tex',  u'Documentation for the Idris Language',    u'The Idris Community', 'report'),+   ('tutorial/index',  'idris-tutorial.tex',  u'The Idris Tutorial',    u'The Idris Community', 'howto'), ]  

@@ -452,7 +452,7 @@     TransEff.Eff  : (t : Type) -> (input_effs : List EFFECT) ->                                   (output_effs : List EFFECT) -> Type     DepEff.Eff    : (t : Type) -> (input_effs : List EFFECT) ->-                                  (output_effs_fn : x -> List EFFECT) -> Type+                                  (output_effs_fn : t -> List EFFECT) -> Type  So far, we have used only the first version, ``SimpleEff.Eff``, which is defined as follows:

@@ -137,7 +137,7 @@  ...which is probably not what was intended!  The reason for this rule is so that it is clear just from looking at the type of ``append``, and no other-context, what the implicitly bound names are. +context, what the implicitly bound names are.  If you want to use an unapplied name in a type, you have two options. You can either explicitly qualify it, for example, if ``ty`` is defined in the@@ -149,7 +149,7 @@  Alternatively, you can use a name which does not begin with a lower case letter, which will never be implicitly bound:-    + .. code-block:: idris      Ty : Type@@ -282,6 +282,11 @@ This answer is based on Edwin Brady's response in the following `pull request <https://github.com/idris-lang/Idris-dev/pull/694#issuecomment-29559291>`__. +Where can I find the community standards for the Idris community?+==================================================================++The Idris Community Standards are stated `here+<https://www.idris-lang.org/documentation/community-standards/>`_ .  Where can I find more answers? ==============================

@@ -1,19 +0,0 @@-.. _faq-index:--##########################-Frequently Asked Questions-##########################--.. note::-   The documentation for Idris has been published under the Creative-   Commons CC0 License. As such to the extent possible under law, *The-   Idris Community* has waived all copyright and related or neighboring-   rights to Documentation for Idris.--   More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/---.. toctree::-   :maxdepth: 1--   faq

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

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

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

@@ -1,3 +1,5 @@+.. _sect-inductive:+ **************** Inductive Proofs ****************

@@ -217,8 +217,129 @@     errno : IO Ptr     errno = foreign FFI_C "&errno" (IO Ptr) -For more complicated interactions with C (such as reading and setting fields of a C struct), there is-a module CFFI available in the contrib package.+If the foreign name is prefixed by a ``#``, the name is pasted in literally. This is+useful to access constants that are preprocessor definitions (like ``INT_MAX``).++.. code-block:: idris++    %include C "limits.h"++    -- access the preprocessor definition INT_MAX+    intMax : IO Int+    intMax = foreign FFI_C "#INT_MAX" (IO Int)++    main : IO ()+    main = print !intMax++For more complicated interactions with C (such as reading and setting fields+of a C struct), there is a module CFFI available in the contrib package.++C heap+------++Idris has two heaps where objects can be allocated:+++--------------------------------------+---------------------------------------++| FP heap                              | C heap                                |++======================================+=======================================++| Cheney-collected                     | Mark-and-sweep-collected              |++--------------------------------------+---------------------------------------++| Garbage collections touches only     | Garbage collection has to traverse    |+| live objects.                        | all registered items.                 |++--------------------------------------+---------------------------------------++| Ideal for FP-style rapid allocation  | Ideal for C-style allocation of a few |+| of lots of small short-lived pieces  | big buffers.                          |+| of memory, such as data constructors.|                                       |++--------------------------------------+---------------------------------------++| Finalizers are impossible to support | Items have finalizers that are called |+| reasonably.                          | on deallocation.                      |++--------------------------------------+---------------------------------------++| Data is copied all the time (when    | Copying does not happen.              |+| collecting garbage, modifying data,  |                                       |+| registering managed pointers, etc.)  |                                       |++--------------------------------------+---------------------------------------++| Contains objects of various types.   | Contains C heap items: ``(void *)``   |+|                                      | pointers with finalizers. A finalizer |+|                                      | is a routine that deallocates the     |+|                                      | resources associated with the item.   |++--------------------------------------+---------------------------------------++| Fixed set of object types.           | The data pointer may point            |+|                                      | to anything, as long as the finalizer |+|                                      | cleans up correctly.                  |++--------------------------------------+---------------------------------------++| Not suitable for C resources and     | Suitable for C resources and arbitrary|+| arbitrary pointers.                  | pointers.                             |++--------------------------------------+---------------------------------------++| Values form a compact memory block.  | Items are kept in a linked list.      |++--------------------------------------+---------------------------------------++| Any Idris value, most notably        | Items represented by the              |+| ``ManagedPtr``.                      | Idris type ``CData``.                 |++--------------------------------------+---------------------------------------++| Data of ``ManagedPtr`` allocated     | Data allocated in C, pointer copied   |+| in C, buffer then copied into the FP | into the C heap.                      |+| heap.                                |                                       |++--------------------------------------+---------------------------------------++| Allocation and reallocation not      | Allocated and reallocate freely in C, |+| possible from C code (without having | registering the allocated items       |+| a reference to the VM). Everything   | in the FFI.                           |+| is copied instead.                   |                                       |++--------------------------------------+---------------------------------------+++The FP heap is the primary heap. It may contain values of type ``CData``,+which are references to items in the C heap. A C heap item contains+a ``(void *)`` pointer and the corresponding finalizer. Once a C heap item+is no longer referenced from the FP heap, it is marked as unused and+the next GC sweep will call its finalizer and deallocate it.++There is no Idris interface for ``CData`` other than its type and FFI.++Usage from C code+~~~~~~~~~~~~~~~~~++* Although not enforced in code, ``CData`` is meant to be opaque+  and non-RTS code (such as libraries or C bindings) should+  access only its ``(void *)`` field called ``data``.++* Feel free to mutate both the pointer ``data`` (eg. after calling ``realloc``)+  and the memory it points to. However, keep in mind+  that this must not break Idris's referential transparency.++* **WARNING!** If you call ``cdata_allocate`` or ``cdata_manage``,+  the resulting ``CData`` object *must* be returned from your+  FFI function so that it is inserted in the C heap by the RTS.+  Otherwise the memory will be leaked.++.. code:: idris++    some_allocating_fun : Int -> IO CData+    some_allocating_fun i = foreign FFI_C "some_allocating_fun" (Int -> IO CData) i++    other_fun : CData -> Int -> IO Int+    other_fun cd i = foreign FFI_C "other_fun" (CData -> Int -> IO Int) cd i++.. code:: cpp++    #include "idris_rts.h"++    static void finalizer(void * data)+    {+        MyStruct * ptr = (MyStruct *) data;+        free_something(ptr->something);+        free(ptr);+    }++    CData some_allocating_fun(int arg)+    {+        void * data = (void *) malloc(...);+        // ...+        return cdata_manage(data, finalizer);+    }++    int other_fun(CData cd, int arg)+    {+        int result = foo(cd->data);+        return result;+    }  FFI implementation ------------------

@@ -113,7 +113,7 @@     Return a highlighted string consisting of the results of making all arguments in serialised term ``TM`` (which would previously have been sent as the ``tt-term`` property of a string) follow their usual implicitness setting.    ``(:elaborate-term TM)``-    Return a highlighted string consisting of the the core language term corresponding to serialised term ``TM`` (which would previously have been sent as the ``tt-term`` property of a string).+    Return a highlighted string consisting of the core language term corresponding to serialised term ``TM`` (which would previously have been sent as the ``tt-term`` property of a string).    ``(:print-definition NAME)``     Return the definition of ``NAME`` as a highlighted string.

@@ -100,113 +100,6 @@                       (x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs))))  -C heap-======--Idris has two heaps where objects can be allocated:--+--------------------------------------+---------------------------------------+-| FP heap                              | C heap                                |-+======================================+=======================================+-| Cheney-collected                     | Mark-and-sweep-collected              |-+--------------------------------------+---------------------------------------+-| Garbage collections touches only     | Garbage collection has to traverse    |-| live objects.                        | all registered items.                 |-+--------------------------------------+---------------------------------------+-| Ideal for FP-style rapid allocation  | Ideal for C-style allocation of a few |-| of lots of small short-lived pieces  | big buffers.                          |-| of memory, such as data constructors.|                                       |-+--------------------------------------+---------------------------------------+-| Finalizers are impossible to support | Items have finalizers that are called |-| reasonably.                          | on deallocation.                      |-+--------------------------------------+---------------------------------------+-| Data is copied all the time (when    | Copying does not happen.              |-| collecting garbage, modifying data,  |                                       |-| registering managed pointers, etc.)  |                                       |-+--------------------------------------+---------------------------------------+-| Contains objects of various types.   | Contains C heap items: ``(void *)``   |-|                                      | pointers with finalizers. A finalizer |-|                                      | is a routine that deallocates the     |-|                                      | resources associated with the item.   |-+--------------------------------------+---------------------------------------+-| Fixed set of object types.           | The data pointer may point            |-|                                      | to anything, as long as the finalizer |-|                                      | cleans up correctly.                  |-+--------------------------------------+---------------------------------------+-| Not suitable for C resources and     | Suitable for C resources and arbitrary|-| arbitrary pointers.                  | pointers.                             |-+--------------------------------------+---------------------------------------+-| Values form a compact memory block.  | Items are kept in a linked list.      |-+--------------------------------------+---------------------------------------+-| Any Idris value, most notably        | Items represented by the              |-| ``ManagedPtr``.                      | Idris type ``CData``.                 |-+--------------------------------------+---------------------------------------+-| Data of ``ManagedPtr`` allocated     | Data allocated in C, pointer copied   |-| in C, buffer then copied into the FP | into the C heap.                      |-| heap.                                |                                       |-+--------------------------------------+---------------------------------------+-| Allocation and reallocation not      | Allocated and reallocate freely in C, |-| possible from C code (without having | registering the allocated items       |-| a reference to the VM). Everything   | in the FFI.                           |-| is copied instead.                   |                                       |-+--------------------------------------+---------------------------------------+--The FP heap is the primary heap. It may contain values of type ``CData``,-which are references to items in the C heap. A C heap item contains-a ``(void *)`` pointer and the corresponding finalizer. Once a C heap item-is no longer referenced from the FP heap, it is marked as unused and-the next GC sweep will call its finalizer and deallocate it.--There is no Idris interface for ``CData`` other than its type and FFI.--Usage from C code--------------------* Although not enforced in code, ``CData`` is meant to be opaque-  and non-RTS code (such as libraries or C bindings) should-  access only its ``(void *)`` field called ``data``.--* Feel free to mutate both the pointer ``data`` (eg. after calling ``realloc``)-  and the memory it points to. However, keep in mind-  that this must not break Idris's referential transparency.--* **WARNING!** If you call ``cdata_allocate`` or ``cdata_manage``,-  the resulting ``CData`` object *must* be returned from your-  FFI function so that it is inserted in the C heap by the RTS.-  Otherwise the memory will be leaked.--.. code:: idris--    some_allocating_fun : Int -> IO CData-    some_allocating_fun i = foreign FFI_C "some_allocating_fun" (Int -> IO CData) i--    other_fun : CData -> Int -> IO Int-    other_fun cd i = foreign FFI_C "other_fun" (CData -> Int -> IO Int) cd i--.. code:: cpp--    #include "idris_rts.h"--    static void finalizer(void * data)-    {-        MyStruct * ptr = (MyStruct *) data;-        free_something(ptr->something);-        free(ptr);-    }--    CData some_allocating_fun(int arg)-    {-        void * data = (void *) malloc(...);-        // ...-        return cdata_manage(data, finalizer);-    }--    int other_fun(CData cd, int arg)-    {-        int result = foo(cd->data);-        return result;-    }- Preorder reasoning ================== 

@@ -91,7 +91,10 @@  + ``makefile = <file>``, which specifies a ``Makefile``, to be built   before the Idris modules, for example to support linking with a-  ``C`` library.+  ``C`` library. When building, Idris sets the environment variables+  ``IDRIS_INCLUDES`` (with C include flags) and ``IDRIS_LDFLAGS``+  (with C linking flags) so they can be used from inside the+  ``Makefile``.  + ``libs = <libs>``, which takes a comma separated list of libraries   which must be present for the package to be usable.

@@ -168,7 +168,7 @@ Records ~~~~~~~ -There is a special syntax for data types with one constructors and+There is a special syntax for data types with one constructor and multiple fields.  .. code:: idris@@ -219,7 +219,7 @@   data Stream : Type -> Type where     (::) a -> Inf (Stream a) -> Stream a -Every occurence of the the defined type in a constructor argument will be+Every occurence of the defined type in a constructor argument will be wrapped in the ``Inf`` type constructor. This has the effect of delaying the evaluation of the second argument when the data constructor is applied. An ``Inf`` argument is constructed using ``Delay`` (which Idris will insert@@ -407,7 +407,6 @@     %no_implicit     %error_handler     %error_reverse-    %assert_total     %reflection     %specialise [<name list>] 

@@ -19,10 +19,10 @@              Type  A value of type ``STrans m resultType in_res out_res_fn`` represents a sequence-of actions which can manipulate state. The arguments are: +of actions which can manipulate state. The arguments are:  * ``m``, which is an underlying *computation context* in which the actions will be executed.-  Usually, this will be a generic type with a ``Monad`` implementation, but +  Usually, this will be a generic type with a ``Monad`` implementation, but   it isn't necessarily so. In particular, there is no need to understand monads   to be able to use ``ST`` effectively! * ``resultType``, which is the type of the value the sequence will produce@@ -76,10 +76,10 @@     same. We'll introduce a much more concise way of writing this type at the     end of this section (:ref:`sttype`), when we describe the ``ST`` type     itself.-                   + This function reads the value stored at the resource ``x`` with ``read``, increments it then writes the result back into the resource ``x`` with-``write``. We'll see the types of ``read`` and ``write`` shortly +``write``. We'll see the types of ``read`` and ``write`` shortly (see :ref:`stransprimops`). We can also create and delete resources:  .. code-block:: idris@@ -104,7 +104,7 @@ ``runPure``. For example, try entering the above definitions in a file ``Intro.idr`` then running the following at the REPL: -.. code:: +.. code::      *Intro> runPure (makeAndIncrement 93)     94 : Integer@@ -179,7 +179,7 @@     Conceptually, at least, you can think of it as having the following type:      .. code-block:: idris-    +         (!) : STrans m a state_in state_out -> a      It is syntactic sugar for binding a variable immediately before the@@ -243,7 +243,7 @@ in any context (as long as it has an implementation of ``Applicative``) and we can execute ``ioMakeAndIncrement`` at the REPL as follows: -.. code:: +.. code::      *Intro> :exec run ioMakeAndIncrement     Enter a number: 93@@ -269,7 +269,7 @@   addElement vec item = do xs <- read vec                            write vec (item :: xs) -Note that you'll need to ``import Data.Vect`` to try this example. +Note that you'll need to ``import Data.Vect`` to try this example.  .. topic:: Updating a state directly with ``update`` @@ -344,7 +344,7 @@ Then, when we implement ``readAndAdd`` we need to return the appropriate value for the output state. If we've added an item to the vector, we need to return ``True``, otherwise we need to return ``False``:-                                                     + .. code-block:: idris    readAndAdd : ConsoleIO io => (vec : Var) ->@@ -435,7 +435,7 @@  .. _stransprimops: -``STrans`` Primitive operations +``STrans`` Primitive operations ===============================  Now that we've written a few small examples of ``STrans`` functions, it's@@ -485,7 +485,7 @@  .. code-block:: idris -    new : (val : state) -> +    new : (val : state) ->           STrans m Var res (\lbl => (lbl ::: State state) :: res)  It's important that the new resource has type ``State state``, rather than@@ -526,7 +526,7 @@  .. code-block:: idris -    returning : (result : ty) -> +    returning : (result : ty) ->                 STrans m () res (const (out_fn result)) ->                 STrans m ty res out_fn @@ -555,7 +555,7 @@ .. _sttype:  `ST`: Representing state transitions directly-============================================+=============================================  We've seen a few examples of small ``STrans`` functions now, and their types can become quite verbose given that we need to provide explicit@@ -568,7 +568,7 @@ .. code-block:: idris      ST : (m : Type -> Type) ->-         (resultType : Type) -> +         (resultType : Type) ->          List (Action resultType) -> Type  ``ST`` is a type level function which computes an appropriate ``STrans``@@ -593,9 +593,9 @@ That is, ``increment`` begins and ends with ``x`` in state ``State Integer``.  .. code-block:: idris-  -  makeAndIncrement : Int -> ST m Int [] +  makeAndIncrement : Integer -> ST m Integer []+ That is, ``makeAndIncrement`` begins and ends with no resources.  .. code-block:: idris@@ -652,5 +652,3 @@ section, we'll see how to use the facilities provided by ``ST`` to write a precise API for a system with security properties: a data store requiring a login.--

@@ -4,7 +4,7 @@ The Idris Tutorial ################## -This is the Idris Tutorial. +This is the Idris Tutorial. It provides a brief introduction to programming in the Idris Language. It covers the core language features, and assumes some familiarity with an existing functional programming language such as Haskell or OCaml.@@ -30,6 +30,7 @@    interp    views    theorems+   provisional    interactive    syntax    miscellany

@@ -48,7 +48,7 @@ Only one implementation of an interface can be given for a type — implementations may not overlap. Implementation declarations can themselves have constraints. To help with resolution, the arguments of an implementation must be-constructors (either data or type constructors) or variables +constructors (either data or type constructors) or variables (i.e. you cannot give an implementation for a function).  For example, to define a ``Show`` implementation for vectors, we need to know that there is a ``Show`` implementation for the element type, because we are@@ -157,7 +157,7 @@ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~  Idris is strictly "define before use", except in ``mutual`` blocks.-In a ``mutual`` block, Idris elaborates in two passes: types on the first +In a ``mutual`` block, Idris elaborates in two passes: types on the first pass and definitions on the second. When the mutual block contains an interface declaration, it elaborates the interface header but none of the method types on the first pass, and elaborates the method types and any@@ -259,7 +259,7 @@     Nothing : Maybe Int  Pattern Matching Bind----------------------+~~~~~~~~~~~~~~~~~~~~~  Sometimes we want to pattern match immediately on the result of a function in ``do`` notation. For example, let's say we have a function ``readNumber``@@ -323,7 +323,7 @@ there may be more than one.  ``!``-notation---------------+~~~~~~~~~~~~~~  In many cases, using ``do``-notation can make programs unnecessarily verbose, particularly in cases such as ``m_add`` above where the value@@ -367,7 +367,7 @@                      f g'  Monad comprehensions---------------------+~~~~~~~~~~~~~~~~~~~~  The list comprehension notation we saw in Section :ref:`sect-more-expr` is more general, and applies to anything which@@ -461,7 +461,7 @@     m_add' x y = [| x + y |]  An error-handling interpreter------------------------------+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~  Idiom notation is commonly useful when defining evaluators. McBride and Paterson describe such an evaluator [1]_, for a language similar

@@ -86,7 +86,7 @@  	fibonacci : {default 0 lag : Nat} -> {default 1 lead : Nat} -> (n : Nat) -> Nat 	fibonacci {lag} Z = lag-	fibonacci {lag} {lead} (S Z) = fibonacci {lag=lead} {lead=lag+lead} n+	fibonacci {lag} {lead} (S n) = fibonacci {lag=lead} {lead=lag+lead} n  After this definition, ``fibonacci 5`` is equivalent to ``fibonacci {lag=0} {lead=1} 5``, and will return the 5th fibonacci number. Note that while this works, this is not the @@ -365,6 +365,14 @@     main : IO ()     main = do          putStrLn $ show $ factorial 3++To compile the generated C with debugging information e.g. to use+``gdb`` to debug segmentation faults in Idris programs, use the+``%flag C`` pragma to include debugging symbols, as is shown below :++.. code-block:: idris++    %flag C "-g"  JavaScript Target =================

@@ -189,8 +189,6 @@     import B     import public C -    public a : AType a = ...- The module ``A`` will export the name ``a``, as well as any public or abstract names in module ``C``, but will not re-export anything from module ``B``.@@ -277,5 +275,3 @@      *params> show (append _ _ (MkVects _ [1,2,3] [4,5,6]))     "[1, 2, 3, 4, 5, 6]" : String--

@@ -11,7 +11,7 @@ of the necessary libraries and tools. You will need:  - A fairly recent version of `GHC <https://www.haskell.org/ghc/>`_. The-  earliest version we currently test with is 7.6.3.+  earliest version we currently test with is 7.10.3.  - The *GNU Multiple Precision Arithmetic Library* (GMP) is available  from MacPorts/Homebrew and all major Linux distributions. 

@@ -33,24 +33,36 @@ the fact that matching on a value in a dependently typed language can affect what we know about the forms of other values. In its simplest form, the ``with`` rule adds another argument to the function being-defined, e.g. we have already seen a vector filter function, defined-as follows:+defined. +We have already seen a vector filter function. This time, we define it+using ``with`` as follows:+ .. code-block:: idris      filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)     filter p [] = ( _ ** [] )     filter p (x :: xs) with (filter p xs)-      | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )+      filter p (x :: xs) | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )  Here, the ``with`` clause allows us to deconstruct the result of-``filter p xs``. Effectively, it adds this value as an extra argument,-which we place after the vertical bar.+``filter p xs``. The view refined argument pattern ``filter p (x ::+xs)`` goes beneath the ``with`` clause, followed by a vertical bar+``|``, followed by the deconstructed intermediate result ``( _ ** xs'+)``. If the view refined argument pattern is unchanged from the+original function argument pattern, then the left side of ``|`` is+extraneous and may be omitted: +.. code-block:: idris++    filter p (x :: xs) with (filter p xs)+      | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )+ If the intermediate computation itself has a dependent type, then the result can affect the forms of other arguments — we can learn the form-of one value by testing another. For example, a ``Nat`` is either even-or odd. If it’s even it will be the sum of two equal ``Nat``.+of one value by testing another. In these cases, view refined argument+patterns must be explicit. For example, a ``Nat`` is either even or+odd. If it is even it will be the sum of two equal ``Nat``. Otherwise, it is the sum of two equal ``Nat`` plus one:  .. code-block:: idris@@ -80,14 +92,29 @@        natToBin (j + j)     | Even = False :: natToBin j        natToBin (S (j + j)) | Odd  = True  :: natToBin j -The value of the result of ``parity k`` affects the form of ``k``,-because the result of ``parity k`` depends on ``k``. So, as well as-the patterns for the result of the intermediate computation (``Even``-and ``odd``) right of the ``|``, we also write how the results-affect the other patterns left of the ``|``. Note that there is-a function in the patterns (``+``) and repeated occurrences of-``j``—this is allowed because another argument has determined the form-of these patterns.+The value of ``parity k`` affects the form of ``k``, because the+result of ``parity k`` depends on ``k``. So, as well as the patterns+for the result of the intermediate computation (``Even`` and ``Odd``)+right of the ``|``, we also write how the results affect the other+patterns left of the ``|``. That is:++- When ``parity k`` evaluates to ``Even``, we can refine the original+  argument ``k`` to a refined pattern ``(j + j)`` according to+  ``Parity (n + n)`` from the ``Even`` constructor definition. So+  ``(j + j)`` replaces ``k`` on the left side of ``|``, and the+  ``Even`` constructor appears on the right side. The natural number+  ``j`` in the refined pattern can be used on the ride side of the+  ``=`` sign.++- Otherwise, when ``parity k`` evaluates to ``Odd``, the original+  argument ``k`` is refined to ``S (j + j)`` according to ``Parity (S+  (n + n))`` from the ``Odd`` constructor definition, and ``Odd`` now+  appears on the ride side of ``|``, again with the natural number+  ``j`` used on the ride side of the ``=`` sign.++Note that there is a function in the patterns (``+``) and repeated+occurrences of ``j`` - this is allowed because another argument has+determined the form of these patterns.  We will return to this function in the next section :ref:`sect-parity` to complete the definition of ``parity``.

binary file changed (326683 → 658507 bytes)

@@ -1,5 +1,5 @@ Name:           idris-Version:        1.1.1+Version:        1.2.0 License:        BSD3 License-file:   LICENSE Author:         Edwin Brady@@ -119,7 +119,7 @@ -- Defaults to True because Hackage is a source release Flag release   Description:  This is an official release-  Default:      False+  Default:      True   manual:       True  Flag freestanding@@ -206,10 +206,11 @@                 , Idris.ModeCommon                 , Idris.Options                 , Idris.Parser+                , Idris.Parser.Data+                , Idris.Parser.Expr                 , Idris.Parser.Helpers                 , Idris.Parser.Ops-                , Idris.Parser.Expr-                , Idris.Parser.Data+                , Idris.Parser.Stack                 , Idris.PartialEval                 , Idris.Primitives                 , Idris.ProofSearch@@ -226,7 +227,6 @@                 , Idris.WhoCalls                 , Idris.CmdOptions -                , IRTS.BCImp                 , IRTS.Bytecode                 , IRTS.CodegenC                 , IRTS.CodegenCommon@@ -250,6 +250,7 @@                  , Idris.Package                 , Idris.Package.Common+                , Idris.Package.Parser                  , Util.DynamicLinker                 , Util.ScreenSize@@ -259,7 +260,7 @@                   Util.Pretty                 , Util.Net -                , Idris.Package.Parser+                                  -- Auto Generated                 , Paths_idris@@ -269,7 +270,7 @@   Build-depends:  base >=4 && <5                 , aeson >= 0.6 && < 1.3                 , annotated-wl-pprint >= 0.7 && < 0.8-                , ansi-terminal < 0.7+                , ansi-terminal < 0.8                 , ansi-wl-pprint < 0.7                 , array >= 0.4.0.1 && < 0.6                 , base64-bytestring < 1.1@@ -286,10 +287,10 @@                 , fingertree >= 0.1 && < 0.2                 , haskeline >= 0.7 && < 0.8                 , ieee754 >= 0.7 && < 0.9+                , megaparsec >= 6.2                 , mtl >= 2.1 && < 2.3                 , network < 2.7                 , optparse-applicative >= 0.13 && < 0.15-                , parsers >= 0.9 && < 0.13                 , pretty < 1.2                 , process < 1.7                 , regex-tdfa >= 1.2@@ -298,9 +299,7 @@                 , terminal-size < 0.4                 , text >=1.2.1.0 && < 1.3                 , time >= 1.4 && < 1.9-                , transformers < 0.6-                , transformers-compat >= 0.3-                , trifecta >= 1.6 && < 1.8+                , transformers >= 0.5 && < 0.6                 , uniplate >=1.6 && < 1.7                 , unordered-containers < 0.3                 , utf8-string < 1.1@@ -310,12 +309,15 @@                 , fsnotify >= 0.2 && < 2.2                 , async < 2.2 +  if !impl(ghc >= 8.0)+    Build-Depends: semigroups == 0.18.*+   Default-Language: Haskell2010   ghc-prof-options: -auto-all -caf-all    if os(windows)      build-depends: mintty >= 0.1 && < 0.2-                  , Win32 < 2.4+                  , Win32 < 2.7   else      build-depends: unix < 2.8   if flag(FFI)@@ -360,7 +362,7 @@                , filepath                , directory                , haskeline >= 0.7-               , optparse-applicative >= 0.11 && < 0.14+               , optparse-applicative >= 0.13 && < 0.15                , tagged                , tasty >= 0.8                , tasty-golden >= 2.0@@ -375,6 +377,7 @@  Executable idris-codegen-c   Main-is:        Main.hs+  other-modules:  Paths_idris   hs-source-dirs: codegen/idris-codegen-c    Build-depends:  idris@@ -389,6 +392,7 @@  Executable idris-codegen-javascript   Main-is:        Main.hs+  other-modules:  Paths_idris   hs-source-dirs: codegen/idris-codegen-javascript    Build-depends:  idris@@ -403,6 +407,7 @@  Executable idris-codegen-node   Main-is:        Main.hs+  other-modules:  Paths_idris   hs-source-dirs: codegen/idris-codegen-node    Build-depends:  idris

@@ -4,7 +4,7 @@  %access public export -interface Category (cat : Type -> Type -> Type) where+interface Category (cat : k -> k -> Type) where   id  : cat a a   (.) : cat b c -> cat a b -> cat a c 

@@ -42,6 +42,10 @@     lift x = ST (\st => do r <- x                            pure (r, st)) +implementation (Monad f, Alternative f) => Alternative (StateT st f) where+    empty = lift empty+    (ST f) <|> (ST g) = ST (\st => f st <|> g st)+ ||| Apply a function to modify the context of this computation modify : MonadState stateType m => (stateType -> stateType) -> m () modify f = do s <- get

@@ -2,7 +2,11 @@  %include C "idris_buffer.h" -||| A buffer is a pointer to a sized, unstructured, mutable chunk of memory+||| A buffer is a pointer to a sized, unstructured, mutable chunk of memory.+||| There are primitive operations for gettng and setting bytes, ints (32 bit) +||| and strings at a location in the buffer. These operations silently fail +||| if the location is out of bounds, so bounds checking should be done in +||| advance. export record Buffer where   constructor MkBuffer@@ -47,6 +51,15 @@     = foreign FFI_C "idris_setBufferByte" (ManagedPtr -> Int -> Bits8 -> IO ())               (rawdata b) loc val +||| Set the int at position 'loc' to 'val'.+||| Uses 4 bytes (assumes up to 32 bit Int).+||| Does nothing if the location is outside the bounds of the buffer+export+setInt : Buffer -> (loc : Int) -> (val : Int) -> IO ()+setInt b loc val+    = foreign FFI_C "idris_setBufferInt" (ManagedPtr -> Int -> Int -> IO ())+              (rawdata b) loc val+ ||| Set the byte at position 'loc' to 'val'. ||| Does nothing if the location is out of bounds of the buffer, or the string ||| is too long for the location@@ -66,12 +79,31 @@     = foreign FFI_C "idris_copyBuffer" (ManagedPtr -> Int -> Int -> ManagedPtr -> Int -> IO ())               (rawdata src) start len (rawdata dest) loc -||| Return the value at the given location in the buffer+||| Return the value at the given location in the buffer.+||| Returns 0 if out of bounds. export getByte : Buffer -> (loc : Int) -> IO Bits8 getByte b loc     = foreign FFI_C "idris_getBufferByte" (ManagedPtr -> Int -> IO Bits8)               (rawdata b) loc ++||| Return the value at the given location in the buffer, assuming 4+||| bytes to store the Int.+||| Returns 0 if out of bounds.+export+getInt : Buffer -> (loc : Int) -> IO Int+getInt b loc+    = foreign FFI_C "idris_getBufferInt" (ManagedPtr -> Int -> IO Int)+              (rawdata b) loc ++||| Return the string at the given location in the buffer, with the given+||| length. Returns "" if out of bounds.+export+getString : Buffer -> (loc : Int) -> (len : Int) -> IO String+getString b loc len+    = do MkRaw str <- foreign FFI_C "idris_getBufferString" (ManagedPtr -> Int -> Int -> IO (Raw String))+                          (rawdata b) loc len+         pure str  ||| Read 'maxbytes' into the buffer from a file, returning a new ||| buffer with the 'locaton' pointer moved along

@@ -70,16 +70,11 @@     (*) (a:+b) (c:+d) = ((a*c-b*d):+(b*c+a*d))     fromInteger x = (fromInteger x:+0) --- We can't do "implementation Neg a => Neg (Complex a)" because--- we need "abs" which needs "magnitude" which needs "sqrt" which needs Double-implementation Neg (Complex Double) where+implementation Neg a => Neg (Complex a) where     negate = map negate     (-) (a:+b) (c:+d) = ((a-c):+(b-d))-    abs (a:+b) = (magnitude (a:+b):+0) --- As soon as abs moves out of Neg (issue #3500), the following would become a--- valid instance:---- implementation Neg a => Neg (Complex a) where---     negate = map negate---     (-) (a:+b) (c:+d) = ((a-c):+(b-d))+-- Specific to Double because `abs` needs `magnitude` which needs `sqrt` which+-- operates on Double.+implementation Abs (Complex Double) where+    abs (a:+b) = (magnitude (a:+b):+0)

@@ -0,0 +1,54 @@+module Data.IORef++export+data IORef a = MkIORef a++public export+interface HasReference (ffi : FFI) where+  newIORef' : a -> IO' ffi (IORef a)+  readIORef' : IORef a -> IO' ffi a+  writeIORef' : IORef a -> a -> IO' ffi ()++export+modifyIORef': HasReference ffi => IORef a -> (a -> a) -> IO' ffi ()+modifyIORef' ref fn =+  do+    val <- readIORef' ref+    writeIORef' ref (fn val)++export+implementation HasReference FFI_C where+  newIORef' val+    = do MkRaw ref <- foreign FFI_C "idris_newRef" (Raw a -> IO (Raw a)) (MkRaw val)+         pure (MkIORef ref)+  readIORef' (MkIORef ref)+    = do MkRaw val <- foreign FFI_C "idris_readRef" (Raw a -> IO (Raw a)) (MkRaw ref)+         pure val+  writeIORef' (MkIORef ref) val+    = foreign FFI_C "idris_writeRef" (Raw a -> Raw a -> IO ())+              (MkRaw ref) (MkRaw val)++export+implementation HasReference FFI_JS where+  newIORef' val =+    (MkIORef . believe_me) <$> foreign FFI_JS "{val: %0}" (Ptr -> JS_IO Ptr) (believe_me val)+  readIORef' (MkIORef ref) =+    believe_me <$> foreign FFI_JS "%0.val" (Ptr -> JS_IO Ptr) (believe_me ref)+  writeIORef' (MkIORef ref) val =+    foreign FFI_JS "%0.val = %1" (Ptr -> Ptr -> JS_IO ()) (believe_me ref) (believe_me val)++export+newIORef : a -> IO (IORef a)+newIORef = newIORef'++export+readIORef : IORef a -> IO a+readIORef = readIORef'++export+writeIORef : IORef a -> a -> IO ()+writeIORef = writeIORef'++export+modifyIORef : IORef a -> (a -> a) -> IO ()+modifyIORef = modifyIORef'

@@ -15,10 +15,31 @@      ||| Example: `the (Elem "b" ["a", "b"]) (There Here)`      There : (later : Elem x xs) -> Elem x (y :: xs) +||| `Here` will never equal `There`.+hereIsNotThere : Not (Here = There _)+hereIsNotThere Refl impossible++||| If the tails don't match, neither will references to them.+tailMismatch : Not (this = that) -> Not (There this = There that)+tailMismatch f Refl = f Refl++implementation DecEq (Elem x xs) where+  decEq Here Here = Yes Refl+  decEq Here (There later) = No hereIsNotThere+  decEq (There later) Here = No (hereIsNotThere . sym)+  decEq (There this) (There that) with (decEq this that)+    decEq (There this) (There this) | Yes Refl  = Yes Refl+    decEq (There this) (There that) | No contra = No (tailMismatch contra)+ implementation Uninhabited (Elem {a} x []) where      uninhabited Here impossible      uninhabited (There p) impossible +||| An item not in the head and not in the tail is not in the List at all+neitherHereNorThere : {x, y : a} -> {xs : List a} -> Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))+neitherHereNorThere xneqy xninxs Here = xneqy Refl+neitherHereNorThere xneqy xninxs (There xinxs) = xninxs xinxs+ ||| Is the given element a member of the given list. ||| ||| @x The element to be tested.@@ -27,15 +48,9 @@ isElem x [] = No absurd isElem x (y :: xs) with (decEq x y)   isElem x (x :: xs) | (Yes Refl) = Yes Here-  isElem x (y :: xs) | (No contra) with (isElem x xs)-    isElem x (y :: xs) | (No contra) | (Yes prf) = Yes (There prf)-    isElem x (y :: xs) | (No contra) | (No f) = No (mkNo contra f)-      where-        mkNo : {xs' : List a} ->-               ((x' = y') -> Void) -> (Elem x' xs' -> Void) ->-               Elem x' (y' :: xs') -> Void-        mkNo f g Here = f Refl-        mkNo f g (There x) = g x+  isElem x (y :: xs) | (No xneqy) with (isElem x xs)+    isElem x (y :: xs) | (No xneqy) | (Yes xinxs) = Yes (There xinxs)+    isElem x (y :: xs) | (No xneqy) | (No xninxs) = No (neitherHereNorThere xneqy xninxs)  ||| Remove the element at the given position. |||

@@ -40,3 +40,15 @@  (~>) : Type -> Type -> Type a ~> b = Morphism a b++Cast (Endomorphism a) (Morphism a a) where+  cast (Endo f) = Mor f++Cast (Morphism a a) (Endomorphism a) where+  cast (Mor f) = Endo f++Monad m => Cast (Morphism a (m b)) (Kleislimorphism m a b) where+  cast (Mor f) = Kleisli f++Cast (Kleislimorphism m a b) (Morphism a (m b)) where+  cast (Kleisli f) = Mor f

@@ -12,9 +12,9 @@        DivByZero : Divides x 0        DivBy : (prf : rem >= 0 && rem < d = True) ->                Divides ((d * div) + rem) d-    +   ||| Covering function for the `Divides` view-  export+  public export   divides : (val : Integer) -> (d : Integer) -> Divides val d   divides val 0 = DivByZero   divides val d@@ -22,21 +22,23 @@              let dividend = if d < 0 then -(val `div` abs d)                                      else val `div` d                  remainder = abs (val - dividend * d) in-                 believe_me (DivBy {d} {div = dividend} {rem = remainder}-                                   (believe_me (Refl {x = True})))+                 really_believe_me (DivBy {d} {div = dividend} {rem = remainder}+                                   (really_believe_me (Refl {x = True})))    ||| View for recursion over Integers+  public export   data IntegerRec : Integer -> Type where        IntegerZ : IntegerRec 0        IntegerSucc : IntegerRec (n - 1) -> IntegerRec n        IntegerPred : IntegerRec ((-n) + 1) -> IntegerRec (-n)-  +   ||| Covering function for `IntegerRec`+  public export   integerRec : (x : Integer) -> IntegerRec x   integerRec 0 = IntegerZ   integerRec x = if x > 0 then IntegerSucc (assert_total (integerRec (x - 1)))-                      else believe_me (IntegerPred {n=-x} -                                (assert_total (believe_me (integerRec (x + 1)))))+                      else really_believe_me (IntegerPred {n=-x}+                                (assert_total (really_believe_me (integerRec (x + 1)))))  namespace Int   ||| View for expressing a number as a multiplication + a remainder@@ -45,13 +47,13 @@        DivByZero : Int.Divides x 0        DivBy : (prf : rem >= 0 && rem < d = True) ->                Int.Divides ((d * div) + rem) d-   +   -- I have assumed, but not actually verified, that this will still   -- give a right result (i.e. still adding up) when the Ints overflow.   -- TODO: Someone please check this and fix if necessary...    ||| Covering function for the `Divides` view-  export+  public export   divides : (val : Int) -> (d : Int) -> Divides val d   divides val 0 = DivByZero   divides val d@@ -59,19 +61,21 @@              let dividend = if d < 0 then -(val `div` abs d)                                      else val `div` d                  remainder = abs (val - dividend * d) in-                 believe_me (DivBy {d} {div = dividend} {rem = remainder}-                                   (believe_me (Refl {x = True})))+                 really_believe_me (DivBy {d} {div = dividend} {rem = remainder}+                                   (really_believe_me (Refl {x = True})))    ||| View for recursion over Ints+  public export   data IntRec : Int -> Type where        IntZ : IntRec 0        IntSucc : IntRec (n - 1) -> IntRec n        IntPred : IntRec ((-n) + 1) -> IntRec (-n)-  +   ||| Covering function for `IntRec`+  public export   intRec : (x : Int) -> IntRec x   intRec 0 = IntZ   intRec x = if x > 0 then IntSucc (assert_total (intRec (x - 1)))-                      else believe_me (IntPred {n=-x}-                                (assert_total (believe_me (intRec (x + 1)))))-  +                      else really_believe_me (IntPred {n=-x}+                                (assert_total (really_believe_me (intRec (x + 1)))))+

@@ -326,10 +326,20 @@ -- Scans -------------------------------------------------------------------------------- +||| The scanl function is similar to foldl, but returns all the intermediate+||| accumulator states in the form of a vector. 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 +||| The scanl1 function is a variant of scanl that doesn't require an explicit+||| 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.+scanl1 : (elem -> elem -> elem) -> Vect len elem -> Vect len elem+scanl1 f [] = []+scanl1 f (x::xs) = scanl f x xs+ -------------------------------------------------------------------------------- -- Membership tests --------------------------------------------------------------------------------@@ -633,6 +643,14 @@ mapElem : {xs : Vect k t} -> {f : t -> u} -> Elem x xs -> Elem (f x) (map f xs) mapElem Here = Here mapElem (There e) = There (mapElem e)++||| Remove the element at the given position.+|||+||| @xs The vector to be removed from+||| @p A proof that the element to be removed is in the vector+dropElem : (xs : Vect (S k) t) -> (p : Elem x xs) -> Vect k t+dropElem (x :: ys) Here = ys+dropElem {k = (S k)} (x :: ys) (There later) = x :: dropElem ys later  -- Some convenience functions for testing lengths 

@@ -308,7 +308,7 @@           my_show d (RApp tm tm') = assert_total $ showCon d "RApp" $ " " ++ my_show App tm ++ " " ++ my_show App tm'           my_show d RType = "RType"           my_show d (RConstant c) = assert_total $ showCon d "RConstant" $ showArg c-          my_show d (RUType u) = "RUType" +          my_show d (RUType u) = "RUType"   implementation Show Err where@@ -387,3 +387,10 @@       showCon d "MkFunClause" $ showArg lhs ++ showArg rhs   showPrec d (MkImpossibleClause lhs) =       showCon d "MkImpossibleClause" $ showArg lhs++implementation Functor FunClause where+  map f (MkFunClause lhs rhs) = MkFunClause (f lhs) (f rhs)+  map f (MkImpossibleClause lhs) = MkImpossibleClause (f lhs)++implementation Functor FunDefn where+  map f (DefineFun n clauses) = DefineFun n (map (map f) clauses)

@@ -97,5 +97,6 @@ usleep : (i : Int) -> { auto prf : So (i >= 0 && i <= 1000000) } -> IO () usleep i = foreign FFI_C "usleep" (Int -> IO ()) i +||| Execute a program and returns its exit status code. system : String -> IO Int system cmd = foreign FFI_C "system" (String -> IO Int) cmd

@@ -1,47 +1,53 @@ package base  opts = "--nobasepkgs --total --no-elim-deprecation-warnings --partial-eval -i ../prelude"-modules = System, -          Debug.Error, Debug.Trace,+modules = Control.Arrow+        , Control.Catchable+        , Control.Category+        , Control.IOExcept+        , Control.Isomorphism -          System.Info,+        , Control.Monad.Identity+        , Control.Monad.Reader+        , Control.Monad.RWS+        , Control.Monad.State+        , Control.Monad.Trans+        , Control.Monad.Writer -          Language.Reflection.Utils,+        , Data.Bits+        , Data.Buffer+        , Data.Complex+        , Data.Erased+        , Data.Fin+        , Data.HVect+        , Data.IORef -          Syntax.PreorderReasoning,+        , Data.List+        , Data.List.Quantifiers+        , Data.List.Views -          Data.Morphisms,-          Data.Bits,-          Data.Mod2,-          Data.Fin,-          Data.Vect,-          Data.Vect.Views,-          Data.Vect.Quantifiers,-          Data.HVect,-          Data.Complex,-          Data.Erased,-          Data.List,-          Data.List.Views,-          Data.List.Quantifiers,-          Data.Nat.Views,-          Data.Primitives.Views,-          Data.String.Views,-          Data.So,-          Data.String,-          Data.Buffer,+        , Data.Mod2+        , Data.Morphisms+        , Data.Nat.Views+        , Data.Primitives.Views+        , Data.So -          Control.Isomorphism,-          Control.Monad.Identity,-          Control.Monad.RWS,-          Control.Monad.Trans,-          Control.Monad.State,-          Control.Monad.Writer,-          Control.Monad.Reader,-          Control.Category,-          Control.Arrow,-          Control.Catchable,-          Control.IOExcept,+        , Data.String+        , Data.String.Views -          System.Concurrency.Raw,-          System.Concurrency.Channels+        , Data.Vect+        , Data.Vect.Quantifiers+        , Data.Vect.Views++        , Debug.Error+        , Debug.Trace++        , Language.Reflection.Utils++        , Syntax.PreorderReasoning++        , System+        , System.Concurrency.Channels+        , System.Concurrency.Raw+        , System.Info

@@ -40,10 +40,11 @@ free (CPt p _ ) = mfree p  ||| Perform an IO action with memory that is freed afterwards-withAlloc : Composite -> (CPtr -> IO ()) -> IO ()+withAlloc : Composite -> (CPtr -> IO a) -> IO a withAlloc t f = do m <- alloc t-                   f m+                   r <- f m                    free m+                   pure r  infixl 1 ~~> ||| Perform an IO action with memory that is freed afterwards

@@ -29,11 +29,11 @@     show PTR = "PTR"  Show Composite where-    show (T ct) = show ct-    show (ARRAY n t) = "ARRAY " ++ show n ++ " " ++ show t-    show (STRUCT xs) = "STRUCT " ++ show xs-    show (UNION xs) = "UNION " ++ show xs-    show (PACKEDSTRUCT xs) = "PACKEDSTRUCT " ++ show xs+    showPrec d (T ct) = showPrec d ct+    showPrec d (ARRAY n t) = showCon d "ARRAY" $ showArg n ++ showArg t+    showPrec d (STRUCT xs) = showCon d "STRUCT" $ showArg xs+    showPrec d (UNION xs) = showCon d "UNION" $ showArg xs+    showPrec d (PACKEDSTRUCT xs) = showCon d "PACKEDSTRUCT" $ showArg xs  ||| What Idris type the C type is marshalled to translate : CType -> Type

@@ -0,0 +1,26 @@+||| Utilities functions for contitionally delaying values.+module Control.Delayed++%default total++||| Type-level function for a conditionally delayed type (`Lazy` or `Inf`).+public export+delayed : DelayReason -> Bool -> Type -> Type+delayed r False a = a+delayed r True a = Delayed r a++||| Type-level function for a conditionally infinite type.+public export+inf : Bool -> Type -> Type+inf = delayed Infinite++||| Type-level function for a conditionally lazy type.+public export+lazy : Bool -> Type -> Type+lazy = delayed LazyValue++||| Conditionally delay a value.+export+delay : (d : Bool) -> a -> delayed r d a+delay False x = x+delay True x = Delay x

@@ -0,0 +1,18 @@+module Control.Monad.Syntax++%default total+%access public export++infixr 1 =<<, <=<, >=>++||| Left-to-right Kleisli composition of monads.+(>=>) : Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)+(>=>) f g = \x => f x >>= g++||| Right-to-left Kleisli composition of monads, flipped version of `>=>`.+(<=<) : Monad m => (b -> m c) -> (a -> m b) -> (a -> m c)+(<=<) = flip (>=>)++||| Right-to-left monadic bind, flipped version of `>>=`.+(=<<) : Monad m => (a -> m b) -> m a -> m b+(=<<) = flip (>>=)

@@ -1,8 +1,10 @@ module Control.ST -import Language.Reflection.Utils import Control.IOExcept+import Language.Reflection.Utils +import public Data.Fuel+ %default total  infix 5 :::@@ -394,13 +396,6 @@ runST env (Read lbl prf) k = k (lookupEnv prf env) env runST env (Write lbl prf val) k = k () (updateEnv prf env val) -export-data Fuel = Empty | More (Lazy Fuel)--export partial-forever : Fuel-forever = More forever- runSTLoop : Fuel -> Env invars -> STransLoop m a invars outfn ->             (k : (x : a) -> Env (outfn x) -> m b) ->             (onDry : m b) -> m b@@ -589,10 +584,10 @@  export runLoop : Applicative m => Fuel -> STLoop m a [] ->-          (onEmpty : m a) ->+          (onDry : m a) ->           m a-runLoop fuel prog onEmpty-    = runSTLoop fuel [] prog (\res, env' => pure res) onEmpty+runLoop fuel prog onDry+    = runSTLoop fuel [] prog (\res, env' => pure res) onDry  ||| runWith allows running an STrans program with an initial environment, ||| which must be consumed.

@@ -0,0 +1,247 @@+module Control.ST.File ++import Control.ST+import Control.IOExcept++%default total++||| A record of the file modes that can read from a file.+public export+data ValidModeRead : Mode -> Type where+  VMRRead   : ValidModeRead Read+  VMRReadW  : ValidModeRead ReadWrite+  VMRReadWT : ValidModeRead ReadWriteTruncate+  VMRReadA  : ValidModeRead ReadAppend++||| A record of the file modes that can write from a file.+public export+data ValidModeWrite : Mode -> Type where+  VMWWrite  : ValidModeWrite WriteTruncate+  VMWAppend : ValidModeWrite Append+  VMWReadW  : ValidModeWrite ReadWrite+  VMWReadWT : ValidModeWrite ReadWriteTruncate++||| The file handle which will be used as a State Transition +||| resource in the `IO` and `IOExcept` implementations of `File`.+|||+||| @mode The `Mode` that the handle was generated under.+|||+public export+data FileHandle : (mode : Mode) -> Type where+  FH : File -> FileHandle mode++||| Description of state transition operations on a file.+|||+||| +------------+-------------+----------------+----------------+----------------++||| | Operation  | State in    | Mode in        | State out      | Mode out       |+||| +------------+-------------+----------------+----------------+----------------++||| | open       | -           | -              | file handle    | input paramater|+||| | close      | file handle | any            | -              | -              |+||| | eof        | file handle | ValidModeRead  | file handle    | ValidModeRead  |+||| | flush      | file handle | any            | file handle    | unchanged      |+||| | readLine   | file handle | ValidModeRead  | file handle    | ValidModeRead  |+||| | readChar   | file handle | ValidModeRead  | file handle    | ValidModeRead  |+||| | readFile   | -           | -              | -              | -              |+||| | writeString| file handle | ValidModeWrite | file handle    | ValidModeWrite |+||| | writeLine  | file handle | ValidModeWrite | file handle    | ValidModeWrite |+||| | writeFile  | -           | -              | -              | -              |+||| +------------+-------------+----------------+----------------+----------------++|||+public export+interface File (m : Type -> Type) where+  FileHandleI : Mode -> Type++  ||| Open a file.+  |||+  ||| @fname the filename.+  ||| @mode  the mode; either Read, WriteTruncate, Append, ReadWrite,+  |||        ReadWriteTruncate, or ReadAppend+  |||+  open     :  (fname : String)+           -> (mode  : Mode)+           -> ST m (Either FileError Var) [ addIfRight (FileHandleI mode) ]++  ||| Close a file.+  close    :  (fileHandle : Var)+           -> ST m () [ remove fileHandle (FileHandleI mode)  ]++  ||| Have we reached the end of the file.+  eof      :  (fileHandle : Var)+           -> {auto prf   : ValidModeRead mode}+           -> ST m Bool [ fileHandle ::: (FileHandleI mode) ]++  ||| Flush+  flush    :  (fileHandle : Var)+           -> ST m () [ fileHandle ::: (FileHandleI mode) ]++  ||| Read a complete line.+  readLine :  (fileHandle : Var)+           -> {auto prf   : ValidModeRead mode}+           -> ST m (Either FileError String) [ fileHandle ::: (FileHandleI mode) ]++  ||| Read a `Char`.+  readChar :  (fileHandle : Var)+           -> {auto prf   : ValidModeRead mode}+           -> ST m (Either FileError Char) [ fileHandle ::: (FileHandleI mode) ]++  ||| Read the contents of a file into a string.+  |||+  ||| This checks the size of+  ||| the file before beginning to read, and only reads that many bytes,+  ||| to ensure that it remains a total function if the file is appended+  ||| to while being read.+  |||+  ||| Returns an error if fname is not a normal file.+  |||+  readFile :  (fileName : String)+           -> ST m (Either FileError String) []++  ||| Write a complete line to the file.+  |||+  ||| @string The string to be written to file.+  |||+  writeString : (fileHandle : Var)+           -> (string     : String) +           -> {auto prf   : ValidModeWrite mode}+           -> ST m (Either FileError ()) [ fileHandle ::: (FileHandleI mode) ]++  ||| Write a complete line to the file.+  |||+  ||| @string The text to be written to file.+  |||+  writeLine : (fileHandle : Var)+           -> (string     : String) +           -> {auto prf   : ValidModeWrite mode}+           -> ST m (Either FileError ()) [ fileHandle ::: (FileHandleI mode) ]++  ||| Create a file and write contents to the file.+  |||+  ||| @fname  The fileName of the file.+  ||| @string The text to be written to file.+  |||+  writeFile : (fname  : String)+           -> (string : String)+           -> ST m (Either FileError ()) []++public export+File IO where+  FileHandleI mode = State (FileHandle mode) ++  open fname mode = do +      (Right file) <- lift ( openFile fname mode )+                   | (Left  error ) => pure (Left error)+      let fh = FH file+      var <- new fh +      pure (Right var)++  close fh = do +      (FH file) <- read fh+      lift (closeFile file)+      delete fh +      pure ()++  eof fh = do  +      (FH file) <- read fh +      isEof <- lift (fEOF file)+      pure (isEof)++  flush fh = do +      (FH file) <- read fh +      lift (fEOF file)+      pure ()++  readLine fh = do +      (FH file) <- read fh +      (Right string) <- lift (fGetLine file)+                     | (Left  error ) => pure (Left error) +      pure (Right string)++  readChar fh = do +      (FH file) <- read fh +      (Right chr) <- lift (fgetc file)+                  | (Left  error ) => pure (Left error) +      pure (Right chr)++  readFile fname = do+      (Right content) <- lift ( readFile fname )+                      | (Left  error ) => pure (Left error) +      pure (Right content)++  writeString fh str = do +      (FH file) <- read fh +      Right x <- lift (fPutStr file str)+              | (Left  error ) => pure (Left error) +      pure (Right x)++  writeLine fh str = do +      (FH file) <- read fh+      Right x <- lift (fPutStrLn file str)+              | (Left  error ) => pure (Left error) +      pure (Right x)++  writeFile fname str = do+      Right x <- lift (writeFile fname str)+              | (Left error ) => pure (Left error) +      pure (Right x)++public export+File (IOExcept a) where+  FileHandleI mode = State (FileHandle mode) ++  open fname mode = do +      (Right file) <- lift (ioe_lift (openFile fname mode))+                   | (Left  error ) => pure (Left error)+      let fh = FH file+      var <- new fh +      pure (Right var)++  close fh = do +      (FH file) <- read fh+      lift (ioe_lift (closeFile file))+      delete fh +      pure ()++  eof fh = do  +      (FH file) <- read fh +      isEof <- lift (ioe_lift (fEOF file))+      pure (isEof)++  flush fh = do +      (FH file) <- read fh +      lift (ioe_lift (fEOF file))+      pure ()++  readLine fh = do +      (FH file) <- read fh +      (Right string) <- lift (ioe_lift (fGetLine file))+                     | (Left  error ) => pure (Left error) +      pure (Right string)++  readChar fh = do +      (FH file) <- read fh +      (Right chr) <- lift (ioe_lift (fgetc file))+                  | (Left  error ) => pure (Left error) +      pure (Right chr)++  readFile fname = do+      (Right content) <- lift (ioe_lift (readFile fname))+                      | (Left  error ) => pure (Left error) +      pure (Right content)++  writeString fh str = do +      (FH file) <- read fh +      Right x <- lift (ioe_lift (fPutStr file str))+              | (Left  error ) => pure (Left error) +      pure (Right x)++  writeLine fh str = do +      (FH file) <- read fh+      Right x <- lift (ioe_lift (fPutStrLn file str))+              | (Left  error ) => pure (Left error) +      pure (Right x)++  writeFile fname str = do+      Right x <- lift (ioe_lift (writeFile fname str))+              | (Left error ) => pure (Left error) +      pure (Right x)+--- EOF -------------------------------------------------------------------------

@@ -0,0 +1,42 @@+module Control.ST.Random++import Control.ST+import Data.Vect++%access public export++Random : Type+Random = State Integer++getRandom : (rnd : Var) -> ST m Integer [rnd ::: Random]+getRandom rnd =+  do+    st <- read rnd+    let st' = assert_total ((1664525 * st + 1013904223) `prim__sremBigInt` (pow 2 32))+    write rnd st'+    pure st'++||| Generates a random Integer in a given range+rndInt : (rnd : Var) -> Integer -> Integer -> ST m Integer [rnd ::: Random]+rndInt rnd lower upper = do v <- getRandom rnd+                            pure $ assert_total ((v `prim__sremBigInt` (upper - lower)) + lower)++||| Generate a random number in `Fin (S k)`+|||+||| Note that rndFin k takes values 0, 1, ..., k.+rndFin : (rnd : Var) -> (k : Nat) -> ST m (Fin (S k)) [rnd ::: Random]+rndFin rnd k = do let v = assert_total $ !(getRandom rnd) `prim__sremBigInt` (cast (S k))+                  pure (toFin v)+ where toFin : Integer -> Fin (S k)+       toFin x = case integerToFin x (S k) of+                      Just v => v+                      Nothing => toFin (assert_smaller x (x - cast (S k)))++||| Select a random element from a vector+rndSelect' : (rnd : Var) -> Vect (S k) a -> ST m a [rnd ::: Random]+rndSelect' {k} rnd xs = pure (Vect.index !(rndFin rnd k)  xs)++||| Select a random element from a non-empty list+rndSelect : (rnd : Var) -> (xs : List a) -> {auto ok : NonEmpty xs} -> ST m a [rnd ::: Random]+rndSelect rnd (x::xs) {ok=NonEmpty} = pure ( !(rndSelect' rnd (x::(fromList xs))))+rndSelect rnd [] {ok=NonEmpty} impossible

@@ -0,0 +1,32 @@+module Data.Bool.Extra++%access public export+%default total++andSameNeutral : (x : Bool) -> x && x = x+andSameNeutral False = Refl+andSameNeutral True = Refl++andFalseFalse : (x : Bool) -> x && False = False+andFalseFalse False = Refl+andFalseFalse True = Refl++andTrueNeutral : (x : Bool) -> x && True = x+andTrueNeutral False = Refl+andTrueNeutral True = Refl++orSameNeutral : (x : Bool) -> x || x = x+orSameNeutral False = Refl+orSameNeutral True = Refl++orFalseNeutral : (x : Bool) -> x || False = x+orFalseNeutral False = Refl+orFalseNeutral True = Refl++orTrueTrue : (x : Bool) -> x || True = True+orTrueTrue False = Refl+orTrueTrue True = Refl++orSameAndRightNeutral : (x, right : Bool) -> x || (x && right) = x+orSameAndRightNeutral False _ = Refl+orSameAndRightNeutral True _ = Refl

@@ -0,0 +1,39 @@+||| Combinators that are thought to be at least situationally useful, mostly for+||| tacit (or point-free) programming. "To Mock a Mockingbird" refers to the book+||| "To Mock a Mockingbird and Other Logic Puzzles: Including an Amazing Adventure+||| in Combinatory Logic", by Raymond Smullyan (which the author of this module+||| hasn't actually read). See+||| http://www.angelfire.com/tx4/cus/combinator/birds.html and+||| https://hackage.haskell.org/package/data-aviary-0.4.0/docs/Data-Aviary-Birds.html+||| an (incomplete?) list of birds introduced. Also includes some operations defined+||| over Arrows.++module Data.Combinators++%default total+%access public export++||| Psi combinator - psi bird (?) - Haskell on.+on : (b -> b -> c) -> (a -> b) -> (a -> a -> c)+on f g x y = g x `f` g y+++infixl 9 ...+||| Blackbird, as named in "To Mock a Mockingbird". This is like+||| function composition, but second function takes two arguments. See the talk+||| "Point-Free or Die: Tacit Programming in Haskell and Beyond" by Amar Shah+||| (https://youtu.be/seVSlKazsNk).+(...) : (c -> d) -> (a -> b -> c) -> (a -> b -> d)+(...) = (.) . (.)++||| Warbler, as named in "To Mock a Mockingbird".+||| See http://code.jsoftware.com/wiki/Vocabulary/tilde+||| Equivalent to `join` on the Reader monad (`(->) e` in Haskell)+reflex : (a -> a -> b) -> (a -> b)+reflex f x = f x x++||| Phoenix, according to Data.Aviary.+||| See http://code.jsoftware.com/wiki/Vocabulary/fork.+||| Equivalent to `liftA2` on the Reader monad (`(->) e` in Haskell)+fork2 : (b -> c -> d) -> (a -> b) -> (a -> c) -> (a -> d)+fork2 f g h x = f (g x) (h x)

@@ -0,0 +1,27 @@+||| Enable applicative-style syntax (Mostly f <$> g <*> h and idiom brackets)+||| for function composition:+module Data.Combinators.Applicative++import Data.Combinators++%default total+%access public export++||| Pure is just const, also known as the K combinator+pure : a -> b -> a+pure = const++||| `map` is (.), but isn't here to discourage that use of the syntax.+||| `foo <$> bar <*> baz` applies `foo` to the results of `bar` and `baz`,+||| and generalizes to multiple arguments.+(<$>) : (b -> c) -> (a -> b) -> (a -> c)+(<$>) f g x = f (g x)++||| Starling, as named in "To Mock a Mockingbird". This is the S combinator.+||| Equivalent to `<*>` on the Reader monad (`(->) e` in Haskell).+||| See http://code.jsoftware.com/wiki/Vocabulary/hook.+(<*>) : (a -> b -> c) -> (a -> b)-> (a -> c)+(<*>) f g x = f x (g x)++liftA2 : (b -> c -> d) -> (a -> b) -> (a -> c) -> (a -> d)+liftA2 = fork2

@@ -0,0 +1,15 @@+||| Combinators from Control.Arrow++first : (a -> b) -> (a, c) -> (b, c)+first f (a, c) = (f a, c)++second : (a -> b) -> ((c, a) -> (c, b))+second f (c, a) = (c, f a)++infixr 3 ***+(***) : (a -> b) -> (a' -> b') -> ((a, a') -> (b, b'))+(***) f g (a, a') = (f a, g a')++infixr 3 &&&+(&&&) : (a -> b) -> (a -> b') -> (a -> (b, b'))+(&&&) f g x = (f x, g x)

@@ -0,0 +1,18 @@+module Data.Fuel++%access public export+%default total++||| Fuel for running total operations potentially indefinitely.+data Fuel = Dry | More (Lazy Fuel)++||| Provide `n` units of fuel.+limit : Nat -> Fuel+limit Z = Dry+limit (S n) = More (limit n)++||| Provide fuel indefinitely.+||| This function is fundamentally partial.+partial+forever : Fuel+forever = More forever

@@ -0,0 +1,47 @@+module Data.IOArray++-- Raw access to IOArrays. This interface is unsafe because there's no+-- bounds checking, and is merely intended to provide primitive access via+-- the RTS. Safe interfaces (either with run time or compile time+-- bounds checking) can be implemented on top of this++-- Implemented entirely by the array primitives in the RTS+data ArrayData : Type -> Type where++export+data IOArray elem = MkIOArray (ArrayData elem)++||| Create a new array of the given size, with all entries set to the+||| given default element.+export+newArray : Int -> elem -> IO (IOArray elem)+newArray size default+    = do vm <- getMyVM+         MkRaw p <- foreign FFI_C "idris_newArray"+                          (Ptr -> Int -> Raw elem -> IO (Raw (ArrayData elem)))+                          vm size (MkRaw default)+         pure (MkIOArray p)++||| Write an element at a location in an array. +||| There is *no* bounds checking, hence this is unsafe. Safe interfaces can+||| be implemented on top of this, either with a run time or compile time+||| check.+export+unsafeWriteArray : IOArray elem -> Int -> elem -> IO ()+unsafeWriteArray (MkIOArray p) i val+    = foreign FFI_C "idris_arraySet"+                    (Raw (ArrayData elem) -> Int -> Raw elem -> IO ())+                    (MkRaw p) i (MkRaw val)++||| Read the element at a location in an array. +||| There is *no* bounds checking, hence this is unsafe. Safe interfaces can+||| be implemented on top of this, either with a run time or compile time+||| check.+export+unsafeReadArray : IOArray elem -> Int -> IO elem+unsafeReadArray (MkIOArray p) i+    = do MkRaw val <- foreign FFI_C "idris_arrayGet"+                              (Raw (ArrayData elem) -> Int -> IO (Raw elem))+                              (MkRaw p) i+         pure val+

@@ -0,0 +1,24 @@+module Data.List.Group++||| The groupBy function returns a list of lists such that the concatenation+||| of the list is equal to the argument, and each sublist contains only+||| elements that are equal according to the user-supplied predicate.+|||+||| ```idris example+||| groupBy (==) [1, 1, 2, 3, 3]+||| ```+|||+groupBy : (a -> a -> Bool) -> List a -> List (List a)+groupBy _ [] = []+groupBy p list@(x :: xs) =+  let (ys, zs) = span (p x) xs in+    (x :: ys) :: groupBy p (assert_smaller list zs)++||| The group function is a special case of groupBy.+|||+||| ```idris example+||| group [1, 1, 2, 3, 3]+||| ```+|||+group : Eq a => List a -> List (List a)+group = groupBy (==)

@@ -0,0 +1,10 @@+module Permutations++-- | All permutations of a list.+permutations : List a -> List (List a)+permutations [] = [[]]+permutations xs = [y :: zs | (y, ys) <- select xs, zs <- permutations ys]+  where+    select : List a -> List (a, List a)+    select []        = []+    select (x :: xs) = (x, xs) :: [(y, x::ys) | (y,ys) <- select xs]

@@ -30,8 +30,10 @@  implementation Neg a => Neg (Vect n a) where   (-) = zipWith (-)-  abs = map abs   negate = map negate++implementation Abs a => Abs (Vect n a) where+  abs = map abs  ----------------------------------------------------------------------- --                        Vector functions

@@ -0,0 +1,16 @@+module Data.Nat.Parity++%access public export++--------------------------------------------------------------------------------+-- Parity+--------------------------------------------------------------------------------++mutual+  even : Nat -> Bool+  even Z = True+  even (S k) = odd k++  odd : Nat -> Bool+  odd Z = False+  odd (S k) = even k

@@ -0,0 +1,13 @@+||| Implicit conversions for erased dependent pairs.+module Data.Pairs.Implicit++%access public export+%default total++||| Convert an Evidence to its proof.+implicit evidence : (x : Exists p) -> p (getWitness x)+evidence = getProof++||| Convert an Element to its value (a.k.a. witness).+implicit element : Subset a p -> a+element = getWitness

@@ -0,0 +1,10 @@+module Data.Stream.Extra++%access public export+%default total++||| Insert elements from a Foldable at the start of an existing Stream+||| @ pfx the Foldable containing elements to prepend+||| @ stream the Stream to prepend the elements to+startWith : Foldable t => (pfx : t a) -> (stream : Stream a) -> Stream a+startWith pfx stream = foldr (\x, xs => x :: xs) stream pfx        

@@ -1,31 +0,0 @@-module Data.String--infixl 5 +>-infixr 5 <+--||| Adds a character to the end of the specified string.-|||-||| ```idris example-||| strSnoc "AB" 'C'-||| ```-||| ```idris example-||| strSnoc "" 'A'-||| ```-strSnoc : String -> Char -> String-strSnoc s c = s ++ (singleton c)--||| Alias of `strSnoc`-|||-||| ```idris example-||| "AB" +> 'C'-||| ```-(+>) : String -> Char -> String-(+>) = strSnoc--||| Alias of `strCons`-|||-||| ```idris example-||| 'A' <+ "AB"-||| ```-(<+) : Char -> String -> String-(<+) = strCons

@@ -0,0 +1,88 @@+module Data.String.Extra++%access public export+%default total++infixl 5 +>+infixr 5 <+++||| Adds a character to the end of the specified string.+|||+||| ```idris example+||| strSnoc "AB" 'C'+||| ```+||| ```idris example+||| strSnoc "" 'A'+||| ```+strSnoc : String -> Char -> String+strSnoc s c = s ++ (singleton c)++||| Alias of `strSnoc`+|||+||| ```idris example+||| "AB" +> 'C'+||| ```+(+>) : String -> Char -> String+(+>) = strSnoc++||| Alias of `strCons`+|||+||| ```idris example+||| 'A' <+ "AB"+||| ```+(<+) : Char -> String -> String+(<+) = strCons++||| Take the first `n` characters from a string. Returns the whole string+||| if it's too short.+take : (n : Nat) -> (input : String) -> String+take n str = substr Z n str++||| Take the last `n` characters from a string. Returns the whole string+||| if it's too short.+takeLast : (n : Nat) -> (input : String) -> String+takeLast n str with (length str)+  takeLast n str | len with (isLTE n len)+    takeLast n str | len | Yes prf = substr (len - n) len str+    takeLast n str | len | No contra = str++||| Remove the first `n` characters from a string. Returns the empty string if+||| the input string is too short.+drop : (n : Nat) -> (input : String) -> String+drop n str = substr n (length str) str++||| Remove the last `n` characters from a string. Returns the empty string if+||| the input string is too short.+dropLast : (n : Nat) -> (input : String) -> String+dropLast n str = reverse (drop n (reverse str))++||| Remove the first and last `n` characters from a string. Returns the empty+||| string if the input string is too short.+shrink : (n : Nat) -> (input : String) -> String+shrink n str = dropLast n (drop n str)++||| Concatenate the strings from a `Foldable` containing strings, separated by+||| the given string.+join : (sep : String) -> Foldable t => (xs : t String) -> String+join sep xs = drop (length sep)+                   (foldl (\acc, x => acc ++ sep ++ x) "" xs)++||| Get a character from a string if the string is long enough.+index : (n : Nat) -> (input : String) -> Maybe Char+index n str with (unpack str)+  index n str | [] = Nothing+  index Z str | (x :: xs) = Just x+  index (S n) str | (x :: xs) = index n str | xs++||| Produce a string by repeating the character `c` `n` times.+replicate : (n : Nat) -> (c : Char) -> String+replicate n c = pack $ replicate n c++||| Indent a given string by `n` spaces.+indent : (n : Nat) -> String -> String+indent n x = replicate n ' ' ++ x++||| Indent each line of a given string by `n` spaces.+indentLines : (n : Nat) -> String -> String+indentLines n str = unlines $ map (indent n) $ lines str+

@@ -24,8 +24,8 @@ absZ (NegS n) = S n  implementation Show ZZ where-  show (Pos n) = show n-  show (NegS n) = "-" ++ show (S n)+  showPrec d (Pos n) = showPrec d n+  showPrec d (NegS n) = showParens (d >= PrefixMinus) $ "-" ++ showPrec PrefixMinus (S n)  negNat : Nat -> ZZ negNat Z = Pos Z@@ -77,6 +77,9 @@   (*) = multZ   fromInteger = fromInt +implementation Abs ZZ where+    abs = cast . absZ+ mutual   implementation Neg ZZ where     negate (Pos Z)     = Pos Z@@ -84,7 +87,6 @@     negate (NegS n)    = Pos (S n)      (-) = subZ-    abs = cast . absZ    ||| Subtract two `ZZ`s. Consider using `(-) {a=ZZ}`.   subZ : ZZ -> ZZ -> ZZ

@@ -0,0 +1,63 @@+module Interfaces.Correlative++import Data.Vect++%access public export+%default total++infixl 3 </>++||| A Correlative functor is a functor where, given `(xs, ys : Correlative f)`,+||| certain elements from xs and ys can be paired with one another due to some+||| intrinsic property of `f`. Elements that cannot be paired are discarded.+interface Functor f => Correlative (f : Type -> Type) where+  (</>) : f (a -> b) -> f a -> f b++infixl 3 </+(</) : Correlative f => f a -> f b -> f a+x </ y = map const x </> y++infixl 3 />+(/>) : Correlative f => f a -> f b -> f b+x /> y = map (const id) x </> y++||| Combine two containers elementwise using some function.+zipWith : Correlative f => (a -> b -> c) -> f a -> f b -> f c+zipWith f xs ys = (map f xs) </> ys++||| Combine three containers elementwise using some function.+zipWith3 : Correlative f => (a -> b -> c -> d) -> f a -> f b -> f c -> f d+zipWith3 f xs ys zs = (map f xs) </> ys </> zs++||| Combine two containers elementwise into a container of pairs.+zip : Correlative f => f a -> f b -> f (a, b)+zip = zipWith (\x, y => (x, y))++||| Combine three containers elementwise into a container of tuples.+zip3 : Correlative f => f a -> f b -> f c -> f (a, b, c)+zip3 = zipWith3 (\x, y, z => (x, y, z))++||| Convert a container of pairs into a pair of containers.+unzip : Functor t => t (a, b) -> (t a, t b)+unzip xs = (map fst xs, map snd xs)++||| Convert a container of tuples into a tuple of containers.+unzip3 : Functor t => t (a, b, c) -> (t a, t b, t c)+unzip3 xs = (map fst xs, unzip (map snd xs))++Correlative Maybe where+  (</>) = (<*>)++Correlative (Either a) where+  (</>) = (<*>)++Correlative List where+  (</>) [] _ = []+  (</>) _ [] = []+  (</>) (f :: fs) (x :: xs) = f x :: (fs </> xs)++Correlative Stream where+  (</>) = (<*>)++Correlative (Vect n) where+  (</>) = (<*>)

@@ -0,0 +1,14 @@+||| The JSON language, as described at http://json.org/+module Language.JSON++import Language.JSON.Lexer+import Language.JSON.Parser++import public Language.JSON.Data++%access export+%default total++||| Parse a JSON string.+parse : String -> Maybe JSON+parse x = parseJSON !(lexJSON x)

@@ -0,0 +1,98 @@+module Language.JSON.Data++import Data.String.Extra++%access private+%default total++public export+data JSON+   = JNull+   | JBoolean Bool+   | JNumber Double+   | JString String+   | JArray (List JSON)+   | JObject (List (String, JSON))++%name JSON json++showChar : Char -> String+showChar c+  = case c of+         '\b' => "\\b"+         '\f' => "\\f"+         '\n' => "\\n"+         '\r' => "\\r"+         '\t' => "\\t"+         '\\' => "\\\\"+         '"'  => "\\\""+         c => if isControl c || c >= '\127'+                 then "\\u" ++ b16ToHexString (fromInteger (cast (ord c)))+                 else singleton c++showString : String -> String+showString x = "\"" ++ concatMap showChar (unpack x) ++ "\""++||| Convert a JSON value into its string representation.+||| No whitespace is added.+stringify : JSON -> String+stringify JNull = "null"+stringify (JBoolean x) = if x then "true" else "false"+stringify (JNumber x) = show x+stringify (JString x) = showString x+stringify (JArray xs) = "[" ++ stringifyValues xs ++ "]"+  where+    stringifyValues : List JSON -> String+    stringifyValues [] = ""+    stringifyValues (x :: xs) = stringify x+                             ++ if isNil xs+                                   then ""+                                   else "," ++ stringifyValues xs+stringify (JObject xs) = "{" ++ stringifyProps xs ++ "}"+  where+    stringifyProp : (String, JSON) -> String+    stringifyProp (key, value) = showString key ++ ":" ++ stringify value++    stringifyProps : List (String, JSON) -> String+    stringifyProps [] = ""+    stringifyProps (x :: xs) = stringifyProp x+                            ++ if isNil xs+                                  then ""+                                  else "," ++ stringifyProps xs++export+Show JSON where+  show = stringify++||| Format a JSON value, indenting by `n` spaces per nesting level.+|||+||| @curr The current indentation amount, measured in spaces.+||| @n The amount of spaces to indent per nesting level.+export+format : {default 0 curr : Nat} -> (n : Nat) -> JSON -> String+format {curr} n json = indent curr $ formatValue curr n json+  where+    formatValue : (curr, n : Nat) -> JSON -> String+    formatValue _ _ (JArray []) = "[]"+    formatValue curr n (JArray xs@(_ :: _)) = "[\n" ++ formatValues xs+                                           ++ indent curr "]"+      where+        formatValues : (xs : List JSON) -> {auto ok : NonEmpty xs} -> String+        formatValues (x :: xs) = format {curr=(curr + n)} n x+                              ++ case nonEmpty xs of+                                      Yes ok => ",\n" ++ formatValues xs+                                      No _ => "\n"+    formatValue _ _ (JObject []) = "{}"+    formatValue curr n (JObject xs@(_ :: _)) = "{\n" ++ formatProps xs+                                            ++ indent curr "}"+      where+        formatProp : (String, JSON) -> String+        formatProp (key, value) = indent (curr + n) (showString key ++ ": ")+                               ++ formatValue (curr + n) n value++        formatProps : (xs : List (String, JSON)) -> {auto ok : NonEmpty xs} -> String+        formatProps (x :: xs) = formatProp x+                             ++ case nonEmpty xs of+                                     Yes ok => ",\n" ++ formatProps xs+                                     No _ => "\n"+    formatValue _ _ x = stringify x

@@ -0,0 +1,40 @@+module Language.JSON.Lexer++import Language.JSON.String+import Text.Lexer+import Text.Token++import public Language.JSON.Tokens++%access private+%default total++numberLit : Lexer+numberLit+  = let sign  = is '-'+        whole = is '0' <|> range '1' '9' <+> many digit+        frac  = is '.' <+> digits+        exp   = like 'e' <+> opt (oneOf "+-") <+> digits in+        opt sign <+> whole <+> opt frac <+> opt exp++jsonTokenMap : TokenMap JSONToken+jsonTokenMap = toTokenMap $+  [ (spaces, JTIgnore)+  , (is ',', JTPunct Comma)+  , (is ':', JTPunct Colon)+  , (is '[', JTPunct $ Square Open)+  , (is ']', JTPunct $ Square Close)+  , (is '{', JTPunct $ Curly Open)+  , (is '}', JTPunct $ Curly Close)+  , (exact "null", JTNull)+  , (exact strTrue <|> exact strFalse, JTBoolean)+  , (numberLit, JTNumber)+  , (permissiveStringLit, JTString)+  ]++export+lexJSON : String -> Maybe (List JSONToken)+lexJSON str+  = case lex jsonTokenMap str of+         (tokens, _, _, "") => Just $ map TokenData.tok tokens+         _ => Nothing

@@ -0,0 +1,71 @@+module Language.JSON.Parser++import Language.JSON.Data+import Text.Parser+import Text.Token++import public Language.JSON.Tokens++%access private+%default total++punct : Punctuation -> Grammar JSONToken True ()+punct p = match $ JTPunct p++rawString : Grammar JSONToken True String+rawString = do mstr <- match JTString+               the (Grammar _ False _) $+                   case mstr of+                        Just str => pure str+                        Nothing => fail "invalid string"++mutual+  json : Grammar JSONToken True JSON+  json = object+     <|> array+     <|> string+     <|> boolean+     <|> number+     <|> null++  object : Grammar JSONToken True JSON+  object = do punct $ Curly Open+              commit+              props <- properties+              punct $ Curly Close+              pure $ JObject props+    where+      properties : Grammar JSONToken False (List (String, JSON))+      properties = sepBy (punct Comma) $+                         do key <- rawString+                            punct Colon+                            value <- json+                            pure (key, value)++  array : Grammar JSONToken True JSON+  array = do punct (Square Open)+             commit+             vals <- values+             punct (Square Close)+             pure (JArray vals)+    where+      values : Grammar JSONToken False (List JSON)+      values = sepBy (punct Comma) json++  string : Grammar JSONToken True JSON+  string = map JString rawString++  boolean : Grammar JSONToken True JSON+  boolean = map JBoolean $ match JTBoolean++  number : Grammar JSONToken True JSON+  number = map JNumber $ match JTNumber++  null : Grammar JSONToken True JSON+  null = map (const JNull) $ match JTNull++export+parseJSON : List JSONToken -> Maybe JSON+parseJSON toks = case parse json $ filter (not . ignored) toks of+                      Right (j, []) => Just j+                      _ => Nothing

@@ -0,0 +1,16 @@+module Language.JSON.String++import Language.JSON.String.Lexer+import Language.JSON.String.Parser+import Language.JSON.String.Tokens+import Text.Lexer++%access export+%default total++permissiveStringLit : Lexer+permissiveStringLit+  = quo <+> manyUntil quo (esc any <|> any) <+> opt quo++stringValue : String -> Maybe String+stringValue x = parseString !(lexString x)

@@ -0,0 +1,38 @@+module Language.JSON.String.Lexer++import Language.JSON.String.Tokens+import Text.Lexer++%access private+%default total++export+quo : Lexer+quo = is '"'++export+esc : Lexer -> Lexer+esc = escape '\\'++unicodeEscape : Lexer+unicodeEscape = esc $ is 'u' <+> count (exactly 4) hexDigit++simpleEscape : Lexer+simpleEscape = esc $ oneOf "\"\\/bfnrt"++legalChar : Lexer+legalChar = non (quo <|> is '\\' <|> control)++jsonStringTokenMap : TokenMap JSONStringToken+jsonStringTokenMap = toTokenMap $+  [ (quo, JSTQuote)+  , (unicodeEscape, JSTUnicodeEscape)+  , (simpleEscape, JSTSimpleEscape)+  , (legalChar, JSTChar)+  ]++export+lexString : String -> Maybe (List JSONStringToken)+lexString x = case lex jsonStringTokenMap x of+                   (toks, _, _, "") => Just $ map TokenData.tok toks+                   _ => Nothing

@@ -0,0 +1,25 @@+module Language.JSON.String.Parser++import Language.JSON.String.Tokens+import Text.Lexer+import Text.Parser++%access private+%default total++stringChar : Grammar JSONStringToken True Char+stringChar = match JSTChar+         <|> match JSTSimpleEscape+         <|> match JSTUnicodeEscape++quotedString : Grammar JSONStringToken True String+quotedString = let q = match JSTQuote in+                   do chars <- between q q (many stringChar)+                      eof+                      pure $ pack chars++export+parseString : List JSONStringToken -> Maybe String+parseString toks = case parse quotedString toks of+                        Right (str, []) => Just str+                        _ => Nothing

@@ -0,0 +1,60 @@+module Language.JSON.String.Tokens++import Data.String.Extra+import Text.Token++%access public export+%default total++data JSONStringTokenKind+  = JSTQuote+  | JSTChar+  | JSTSimpleEscape+  | JSTUnicodeEscape++JSONStringToken : Type+JSONStringToken = Token JSONStringTokenKind++Eq JSONStringTokenKind where+  (==) JSTQuote JSTQuote = True+  (==) JSTChar JSTChar = True+  (==) JSTSimpleEscape JSTSimpleEscape = True+  (==) JSTUnicodeEscape JSTUnicodeEscape = True+  (==) _ _ = False++private+charValue : String -> Char+charValue x = case index 0 x of+                   Nothing => '\NUL'+                   Just c  => c++private+simpleEscapeValue : String -> Char+simpleEscapeValue x+  = case index 1 x of+         Nothing => '\NUL'+         Just c => case c of+                        '"'  => '"'+                        '\\' => '\\'+                        '/'  => '/'+                        'b'  => '\b'+                        'f'  => '\f'+                        'n'  => '\n'+                        'r'  => '\r'+                        't'  => '\t'+                        _    => '\NUL'++private+unicodeEscapeValue : String -> Char+unicodeEscapeValue x = chr $ cast ("0x" ++ drop 2 x)++TokenKind JSONStringTokenKind where+  TokType JSTQuote = ()+  TokType JSTChar = Char+  TokType JSTSimpleEscape = Char+  TokType JSTUnicodeEscape = Char++  tokValue JSTQuote = const ()+  tokValue JSTChar = charValue+  tokValue JSTSimpleEscape = simpleEscapeValue+  tokValue JSTUnicodeEscape = unicodeEscapeValue

@@ -0,0 +1,72 @@+module Language.JSON.Tokens++import Language.JSON.String+import Text.Token++%access public export+%default total++strTrue : String+strTrue = "true"++strFalse : String+strFalse = "false"++data Bracket = Open | Close++Eq Bracket where+  (==) Open Open = True+  (==) Close Close = True+  (==) _ _ = False++data Punctuation+  = Comma+  | Colon+  | Square Bracket+  | Curly Bracket++Eq Punctuation where+  (==) Comma Comma = True+  (==) Colon Colon = True+  (==) (Square b1) (Square b2) = b1 == b2+  (==) (Curly b1) (Curly b2) = b1 == b2+  (==) _ _ = False++data JSONTokenKind+  = JTBoolean+  | JTNumber+  | JTString+  | JTNull+  | JTPunct Punctuation+  | JTIgnore++JSONToken : Type+JSONToken = Token JSONTokenKind++Eq JSONTokenKind where+  (==) JTBoolean JTBoolean = True+  (==) JTNumber JTNumber = True+  (==) JTString JTString = True+  (==) JTNull JTNull = True+  (==) (JTPunct p1) (JTPunct p2) = p1 == p2+  (==) _ _ = False++TokenKind JSONTokenKind where+  TokType JTBoolean = Bool+  TokType JTNumber = Double+  TokType JTString = Maybe String+  TokType JTNull = ()+  TokType (JTPunct _) = ()+  TokType JTIgnore = ()++  tokValue JTBoolean x = x == strTrue+  tokValue JTNumber x = cast x+  tokValue JTString x = stringValue x+  tokValue JTNull _ = ()+  tokValue (JTPunct _) _ = ()+  tokValue JTIgnore _ = ()++export+ignored : JSONToken -> Bool+ignored (Tok JTIgnore _) = True+ignored _ = False

@@ -8,10 +8,6 @@ import Network.Socket.Raw  %include C "idris_net.h"-%include C "sys/types.h"-%include C "sys/socket.h"-%include C "unistd.h"-%include C "netdb.h"  %access export @@ -24,7 +20,7 @@       -> (pnum : ProtocolNumber)       -> IO (Either SocketError Socket) socket sf st pn = do-  socket_res <- foreign FFI_C "socket"+  socket_res <- foreign FFI_C "idrnet_socket"                         (Int -> Int -> Int -> IO Int)                         (toCode sf) (toCode st) pn 

@@ -8,9 +8,6 @@ import public Network.Socket.Data  %include C "idris_net.h"-%include C "sys/types.h"-%include C "sys/socket.h"-%include C "netdb.h"  %access public export 

@@ -0,0 +1,14 @@+-- ---------------------------------------------------------------- [ Unit.idr ]+-- Module    : Unit.idr+-- Copyright : (c) The Idris Community.+-- License   : see LICENSE+-- --------------------------------------------------------------------- [ EOH ]+||| A simple Unit testing framework.+module Test.Unit++import public Test.Unit.Display+import public Test.Unit.Generic+import public Test.Unit.Assertions+import public Test.Unit.Runners++-- --------------------------------------------------------------------- [ EOF ]

@@ -0,0 +1,37 @@+-- ---------------------------------------------------------- [ Assertions.idr ]+-- Module    : Assertions.idr+-- Copyright : (c) The Idris Community+-- License   : see LICENSE+-- --------------------------------------------------------------------- [ EOH ]+||| Some simple assertions.+module Test.Unit.Assertions++import Test.Unit.Generic++%access export++assertTrue : (given : Bool) -> IO Bool+assertTrue b = genericTest (Just "Assert True") b True (==)++assertFalse : (given : Bool) -> IO Bool+assertFalse b = genericTest (Just "Assert False") b False (==)++assertEquals : (Eq a, Show a) => (given : a) -> (expected : a) -> IO Bool+assertEquals g e = genericTest (Just "Assert Equals") g e (==)++assertNotEquals : (Eq a, Show a) => (given : a) -> (expected : a) -> IO Bool+assertNotEquals g e = genericTest (Just "Assert Not Equals") g e (\x,y => not (x == y))++assertJust : Show a => (given : Maybe a) -> IO Bool+assertJust g = genericTest (Just "Assert Is Just") (isJust g) True (==)++assertNothing : Show a => (given : Maybe a) -> IO Bool+assertNothing g = genericTest (Just "Assert Is Nothing") (isNothing g) True (==)++assertLeft : (Show a, Show b) => (given : Either a b) -> IO Bool+assertLeft g = genericTest (Just "Assert is Left") (isLeft g) True (==)++assertRight : (Show a, Show b) => (given : Either a b) -> IO Bool+assertRight g = genericTest (Just "Assert is Right") (isRight g) True (==)++-- --------------------------------------------------------------------- [ EOF ]

@@ -0,0 +1,27 @@+-- ------------------------------------------------------------- [ Display.idr ]+-- Module    : Display.idr+-- Copyright : (c) The Idris Community.+-- License   : see LICENSE+-- --------------------------------------------------------------------- [ EOH ]+||| Some simple utilities to make the display fancier.+module Test.Unit.Display++%access export++fancyLine : Nat -> Char -> String+fancyLine l c = pack $ replicate l c++infoLine : String+infoLine = fancyLine 40 '-'++succLine : String+succLine = fancyLine 40 '='++errLine : String+errLine = fancyLine 40 '+'++heading : String -> String+heading n = unlines [infoLine, n, infoLine]+++-- --------------------------------------------------------------------- [ EOF ]

@@ -0,0 +1,43 @@+-- ------------------------------------------------------------- [ Generic.idr ]+-- Module    : Generic.idr+-- Copyright : (c) The Idris Community+-- License   : see LICENSE+-- --------------------------------------------------------------------- [ EOH ]+||| Generic Tests+module Test.Unit.Generic++import Text.PrettyPrint.WL++import Test.Unit.Display++%default total+%access export++||| Run a generic test.+|||+||| @title     Optional Test title+||| @given     The given string to parse+||| @expected  The expected result+||| @tFunc     The testing function to compare the results.+genericTest : Show a+           => (title : Maybe String)+           -> (given : a)+           -> (expected : a)+           -> (tFunc : a -> a -> Bool)+           -> IO Bool+genericTest title g e eq = do+  putStrLn $ unwords ["Test:" , fromMaybe "Unnamed Test" title]+  let res = eq g e+  when (not res) $ do+     let errMsg = vcat [+           text errLine+         , text "An error occured" <+> colon+         , indent 2 $ text "Given" <+> colon+         , indent 4 $ text (show g)+         , indent 2 $ text "Expected" <+> colon+         , indent 4 $ text (show e)+         , text errLine]+     putStrLn $ Default.toString errMsg+  pure res++-- --------------------------------------------------------------------- [ EOF ]

@@ -0,0 +1,36 @@+-- ------------------------------------------------------------- [ Runners.idr ]+-- Module    : Runners.idr+-- Copyright : (c) The Idris Community.+-- License   : see LICENSE+-- --------------------------------------------------------------------- [ EOH ]+||| Given a series of tests, execute them and report results.+module Test.Unit.Runners++import Test.Unit.Display++%default total+%access export++namespace NonReporting+  ||| Run the given set of tests, but don't return the results.+  runTests : List (IO Bool) -> IO ()+  runTests Nil = do+           putStrLn "All Tests have been performed."+           putStrLn succLine+  runTests (t::ts) = do t; runTests ts++namespace Reporting+  ||| Run the given set of tests and return the results.+  runTests : List (IO Bool) -> IO (List Bool)+  runTests Nil = do+    putStrLn "All tests have been performed."+    putStrLn succLine+    pure Nil+  runTests (x::xs) = do+       r  <- x+       rs <- Reporting.runTests xs+       pure (r::rs)++++-- --------------------------------------------------------------------- [ EOF ]

@@ -1,248 +1,300 @@ module Text.Lexer +import Data.Bool.Extra++import public Text.Lexer.Core+import public Text.Quantity+import public Text.Token++%access export %default total -||| A language of token recognisers.-||| The `consumes` flag is True is the recogniser is guaranteed to consume-||| at least one character-export-data Recognise : (consumes : Bool) -> Type where-     Empty : Recognise False-     Fail : Recognise c-     Pred : (Char -> Bool) -> Recognise True-     SeqEat : Recognise True -> Inf (Recognise e) -> Recognise True-     SeqEmpty : Recognise e1 -> Recognise e2 -> Recognise (e1 || e2)-     Alt : Recognise e1 -> Recognise e2 -> Recognise (e1 && e2)+toTokenMap : List (Lexer, k) -> TokenMap (Token k)+toTokenMap = map $ \(l, kind) => (l, Tok kind) -||| A token recogniser. Guaranteed to consume at least one character.-public export-Lexer : Type-Lexer = Recognise True+||| Recognise any character.+||| /./+any : Lexer+any = pred (const True) -public export-inf : Bool -> Type -> Type-inf True t = Inf t-inf False t = t+||| Recognise a lexer or recognise no input. This is not guaranteed+||| to consume input.+||| /`l`?/+opt : (l : Lexer) -> Recognise False+opt l = l <|> empty -||| Sequence two recognisers. If either consumes a character, the sequence-||| is guaranteed to consume a character.-export %inline-(<+>) : {c1 : Bool} ->-        Recognise c1 -> inf c1 (Recognise c2) -> Recognise (c1 || c2)-(<+>) {c1 = False} = SeqEmpty-(<+>) {c1 = True} = SeqEat+||| Recognise any character if the sub-lexer `l` fails.+||| /(?!`l`)./+non : (l : Lexer) -> Lexer+non l = reject l <+> any -||| Alternative recognisers. If both consume, the combination is guaranteed-||| to consumer a character.-export-(<|>) : Recognise c1 -> Recognise c2 -> Recognise (c1 && c2)-(<|>) = Alt+||| Produce recognisers by applying a function to elements of a container, and+||| recognise the first match. Consumes input if the function produces consuming+||| recognisers. Fails if the container is empty.+choiceMap : {c : Bool} ->+            Foldable t => (a -> Recognise c) -> t a -> Recognise c+choiceMap {c} f xs = foldr (\x, acc => rewrite sym (andSameNeutral c) in+                                               f x <|> acc)+                           fail xs -||| Recognise a specific character-export-is : Char -> Lexer-is x = Pred (==x)+||| Recognise the first matching recogniser in a container. Consumes input if+||| recognisers in the list consume. Fails if the container is empty.+choice : Foldable t => t (Recognise c) -> Recognise c+choice = choiceMap id -||| Recognise anything but the given character-export-isNot : Char -> Lexer-isNot x = Pred (/=x)+||| Sequence a list of recognisers. Guaranteed to consume input if the list is+||| non-empty and the recognisers consume.+concat : (xs : List (Recognise c)) -> Recognise (c && isCons xs)+concat = concatMap id -||| Recognise a sequence of at least one sub-lexers-export-some : Lexer -> Lexer-some l = l <+> (some l <|> Empty)+||| Recognise a specific character.+||| /[`x`]/+is : (x : Char) -> Lexer+is x = pred (==x) -||| Recognise a sequence of at zero or more sub-lexers. This is not-||| guaranteed to consume input-export-many : Lexer -> Recognise False-many l = some l <|> Empty+||| Recognise anything but the given character.+||| /[\^`x`]/+isNot : (x : Char) -> Lexer+isNot x = pred (/=x) +||| Recognise a specific character (case-insensitive).+||| /[`x`]/i+like : (x : Char) -> Lexer+like x = pred (\y => toUpper x == toUpper y)++||| Recognise anything but the given character (case-insensitive).+||| /[\^`x`]/i+notLike : (x : Char) -> Lexer+notLike x = pred (\y => toUpper x /= toUpper y)++||| Recognise a specific string.+||| Fails if the string is empty.+||| /`str`/+exact : (str : String) -> Lexer+exact str = case unpack str of+                 [] => fail+                 (x :: xs) => concatMap is (x :: xs)++||| Recognise a specific string (case-insensitive).+||| Fails if the string is empty.+||| /`str`/i+approx : (str : String) -> Lexer+approx str = case unpack str of+                  [] => fail+                  (x :: xs) => concatMap like (x :: xs)++||| Recognise any of the characters in the given string.+||| /[`chars`]/+oneOf : (chars : String) -> Lexer+oneOf chars = pred (\x => x `elem` unpack chars)++||| Recognise a character range. Also works in reverse!+||| /[`start`-`end`]/+range : (start : Char) -> (end : Char) -> Lexer+range start end = pred (\x => (x >= min start end)+                           && (x <= max start end))++mutual+  ||| Recognise a sequence of at least one sub-lexers+  ||| /`l`+/+  some : Lexer -> Lexer+  some l = l <+> many l++  ||| Recognise a sequence of at zero or more sub-lexers. This is not+  ||| guaranteed to consume input+  ||| /`l`\*/+  many : Lexer -> Recognise False+  many l = opt (some l)++||| Repeat the sub-lexer `l` zero or more times until the lexer+||| `stopBefore` is encountered. `stopBefore` will not be consumed.+||| Not guaranteed to consume input.+||| /((?!`stopBefore`)`l`)\*/+manyUntil : (stopBefore : Recognise c) -> (l : Lexer) -> Recognise False+manyUntil stopBefore l = many (reject stopBefore <+> l)++||| Repeat the sub-lexer `l` zero or more times until the lexer+||| `stopAfter` is encountered, and consume it. Guaranteed to+||| consume if `stopAfter` consumes.+||| /`l`\*?`stopAfter`/+manyThen : (stopAfter : Recognise c) -> (l : Lexer) -> Recognise c+manyThen stopAfter l = manyUntil stopAfter l <+> stopAfter+ ||| Recognise many instances of `l` until an instance of `end` is ||| encountered. ||| ||| Useful for defining comments.-export-manyTill : (l : Lexer)-        -> (end : Lexer) -> Recognise False-manyTill l end = end-             <|> (l <+> manyTill l end)-             <|> Empty+manyTill : (l : Lexer) -> (end : Lexer) -> Recognise False+manyTill l end = end <|> opt (l <+> manyTill l end)+%deprecate manyTill+    "Prefer `lineComment`, or `manyUntil`/`manyThen` (argument order is flipped)." -||| Recognise any character-export-any : Lexer-any = Pred (const True)+||| Recognise a sub-lexer repeated as specified by `q`. Fails if `q` has+||| `min` and `max` in the wrong order. Consumes input unless `min q` is zero.+||| /`l`{`q`}/+count : (q : Quantity) -> (l : Lexer) -> Recognise (isSucc (min q))+count (Qty Z Nothing) l = many l+count (Qty Z (Just Z)) _ = empty+count (Qty Z (Just (S max))) l = opt $ l <+> count (atMost max) l+count (Qty (S min) Nothing) l = l <+> count (atLeast min) l+count (Qty (S min) (Just Z)) _ = fail+count (Qty (S min) (Just (S max))) l = l <+> count (between min max) l -||| Recognise no input (doesn't consume any input)-export-empty : Recognise False-empty = Empty+||| Recognise a single digit 0-9+||| /[0-9]/+digit : Lexer+digit = pred isDigit -||| Recognise a character that matches a predicate-export-pred : (Char -> Bool) -> Lexer-pred = Pred+||| Recognise one or more digits +||| /[0-9]+/+digits : Lexer+digits = some digit -||| Recognise any of the characters in the given string-export-oneOf : String -> Lexer-oneOf cs = pred (\x => x `elem` unpack cs)+||| Recognise a single hexidecimal digit+||| /[0-9A-Fa-f]/+hexDigit : Lexer+hexDigit = pred isHexDigit -data StrLen : Type where-     MkStrLen : String -> Nat -> StrLen+||| Recognise one or more hexidecimal digits+||| /[0-9A-Fa-f]+/+hexDigits : Lexer+hexDigits = some hexDigit -getString : StrLen -> String-getString (MkStrLen str n) = str+||| Recognise a single alpha character+||| /[A-Za-z]/+alpha : Lexer+alpha = pred isAlpha -strIndex : StrLen -> Nat -> Maybe Char-strIndex (MkStrLen str len) i-    = if i >= len then Nothing-                  else Just (assert_total (prim__strIndex str (cast i)))+||| Recognise one or more alpha characters+||| /[A-Za-z]+/+alphas : Lexer+alphas = some alpha -mkStr : String -> StrLen-mkStr str = MkStrLen str (length str)+||| Recognise a lowercase alpha character+||| /[a-z]/+lower : Lexer+lower = pred isLower -strTail : Nat -> StrLen -> StrLen-strTail start (MkStrLen str len)-    = MkStrLen (substr start len str) (minus len start)+||| Recognise one or more lowercase alpha characters+||| /[a-z]+/+lowers : Lexer+lowers = some lower --- If the string is recognised, returns the index at which the token--- ends-scan : Recognise c -> Nat -> StrLen -> Maybe Nat-scan Empty idx str = pure idx-scan Fail idx str = Nothing-scan (Pred f) idx str-    = do c <- strIndex str idx-         if f c-            then Just (idx + 1)-            else Nothing-scan (SeqEat r1 r2) idx str-    = do idx' <- scan r1 idx str-         -- TODO: Can we prove totality instead by showing idx has increased?-         assert_total (scan r2 idx' str)-scan (SeqEmpty r1 r2) idx str-    = do idx' <- scan r1 idx str-         scan r2 idx' str-scan (Alt r1 r2) idx str-    = case scan r1 idx str of-           Nothing => scan r2 idx str-           Just idx => Just idx+||| Recognise an uppercase alpha character+||| /[A-Z]/+upper : Lexer+upper = pred isUpper -takeToken : Lexer -> StrLen -> Maybe (String, StrLen)-takeToken lex str-    = do i <- scan lex 0 str -- i must be > 0 if successful-         pure (substr 0 i (getString str), strTail i str)+||| Recognise one or more uppercase alpha characters+||| /[A-Z]+/+uppers : Lexer+uppers = some upper -||| Recognise a digit 0-9-export-digits : Lexer-digits = some (Pred isDigit)+||| Recognise an alphanumeric character+||| /[A-Za-z0-9]/+alphaNum : Lexer+alphaNum = pred isAlphaNum -||| Recognise a specific string-export-exact : String -> Lexer-exact str with (unpack str)-  exact str | [] = Fail -- Not allowed, Lexer has to consume-  exact str | (x :: xs)-      = foldl SeqEmpty (is x) (map is xs)+||| Recognise one or more alphanumeric characters+||| /[A-Za-z0-9]+/+alphaNums : Lexer+alphaNums = some alphaNum -||| Recognise a whitespace character-export+||| Recognise a single whitespace character+||| /\\s/ space : Lexer-space = some (pred isSpace)+space = pred isSpace -||| Recognise a non-alphanumeric, non-whitespace character-export+||| Recognise one or more whitespace characters+||| /\\s+/+spaces : Lexer+spaces = some space++||| Recognise a single newline sequence. Understands CRLF, CR, and LF+||| /\\r\\n|[\\r\\n]/+newline : Lexer+newline = let crlf = "\r\n" in+              exact crlf <|> oneOf crlf++||| Recognise one or more newline sequences. Understands CRLF, CR, and LF+||| /(\\r\\n|[\\r\\n])+)/+newlines : Lexer+newlines = some newline++||| Recognise a single non-whitespace, non-alphanumeric character+||| /[\^\\sA-Za-z0-9]/ symbol : Lexer-symbol = some (pred (\x => not (isAlphaNum x) && not (isSpace x)))+symbol = pred (\x => not (isSpace x || isAlphaNum x)) -strChar : Lexer-strChar = (is '\\' <+> any) <|> isNot '"'+||| Recognise one or more non-whitespace, non-alphanumeric characters+||| /[\^\\sA-Za-z0-9]+/+symbols : Lexer+symbols = some symbol +||| Recognise a single control character+||| /[\\x00-\\x1f\\x7f-\\x9f]/+control : Lexer+control = pred isControl++||| Recognise one or more control characters+||| /[\\x00-\\x1f\\x7f-\\x9f]+/+controls : Lexer+controls = some control++||| Recognise zero or more occurrences of a sub-lexer between+||| delimiting lexers+||| /`start`(`l`)\*?`end`/+surround : (start : Lexer) -> (end : Lexer) -> (l : Lexer) -> Lexer+surround start end l = start <+> manyThen end l++||| Recognise zero or more occurrences of a sub-lexer surrounded+||| by the same quote lexer on both sides (useful for strings)+||| /`q`(`l`)\*?`q`/+quote : (q : Lexer) -> (l : Lexer) -> Lexer+quote q l = surround q q l++||| Recognise an escape character (often '\\') followed by a sub-lexer+||| /[`esc`]`l`/+escape : (esc : Char) -> Lexer -> Lexer+escape esc l = is esc <+> l+ ||| Recognise a string literal, including escaped characters. ||| (Note: doesn't yet handle escape sequences such as \123)-export+||| /"(\\\\.|.)\*?"/ stringLit : Lexer-stringLit = is '"' <+> many strChar <+> is '"'+stringLit = quote (is '"') (escape '\\' any <|> any)  ||| Recognise a character literal, including escaped characters. ||| (Note: doesn't yet handle escape sequences such as \123)-export+||| /'(\\\\.|[\^'])'/ charLit : Lexer-charLit = is '\'' <+> strChar <+> is '\''+charLit = let q = '\'' in+              is q <+> (escape '\\' any <|> isNot q) <+> is q  ||| Recognise an integer literal (possibly with a '-' prefix)-export+||| /-?[0-9]+/ intLit : Lexer-intLit = (is '-' <|> Empty) <+> digits--||| A mapping from lexers to the tokens they produce.-||| This is a list of pairs `(Lexer, String -> tokenType)`-||| For each Lexer in the list, if a substring in the input matches, run-||| the associated function to produce a token of type `tokenType`-public export-TokenMap : (tokenType : Type) -> Type-TokenMap tokenType = List (Lexer, String -> tokenType)--||| A token, and the line and column where it was in the input-public export-record TokenData a where-  constructor MkToken-  line : Int-  col : Int-  tok : a+intLit = opt (is '-') <+> digits -fspanEnd : Nat -> (Char -> Bool) -> String -> (Nat, String)-fspanEnd k p "" = (k, "")-fspanEnd k p xxs-    = assert_total $-      let x = prim__strHead xxs-          xs = prim__strTail xxs in-          if p x then fspanEnd (S k) p xs-                 else (k, xxs)+||| Recognise a hexidecimal literal, prefixed by "0x" or "0X"+||| /0[Xx][0-9A-Fa-f]+/+hexLit : Lexer+hexLit = approx "0x" <+> hexDigits --- Faster version of 'span' from the prelude (avoids unpacking)-export-fspan : (Char -> Bool) -> String -> (String, String)-fspan p xs-    = let (end, rest) = fspanEnd 0 p xs in-          (substr 0 end xs, rest)+||| Recognise `start`, then recognise all input until a newline is encountered,+||| and consume the newline. Will succeed if end-of-input is encountered before+||| a newline.+||| /`start`[\^\\r\\n]+(\\r\\n|[\\r\\n])?/+lineComment : (start : Lexer) -> Lexer+lineComment start = start <+> manyUntil newline any <+> opt newline -tokenise : (line : Int) -> (col : Int) ->-           List (TokenData a) -> TokenMap a ->-           StrLen -> (List (TokenData a), (Int, Int, StrLen))-tokenise line col acc tmap str-    = case getFirstToken tmap str of-           Just (tok, line', col', rest) =>-           -- assert total because getFirstToken must consume something-                assert_total (tokenise line' col' (tok :: acc) tmap rest)-           Nothing => (reverse acc, (line, col, str))+||| Recognise all input between `start` and `end` lexers.+||| Supports balanced nesting.+|||+||| For block comments that don't support nesting (such as C-style comments),+||| use `surround`+blockComment : (start : Lexer) -> (end : Lexer) -> Lexer+blockComment start end = start <+> middle <+> end   where-    countNLs : List Char -> Nat-    countNLs str = List.length (filter (== '\n') str)--    getCols : String -> Int -> Int-    getCols x c-         = case fspan (/= '\n') (reverse x) of-                (incol, "") => c + cast (length incol)-                (incol, _) => cast (length incol)--    getFirstToken : TokenMap a -> StrLen -> Maybe (TokenData a, Int, Int, StrLen)-    getFirstToken [] str = Nothing-    getFirstToken ((lex, fn) :: ts) str-        = case takeToken lex str of-               Just (tok, rest) => Just (MkToken line col (fn tok),-                                         line + cast (countNLs (unpack tok)),-                                         getCols tok col, rest)-               Nothing => getFirstToken ts str--||| Given a mapping from lexers to token generating functions (the-||| TokenMap a) and an input string, return a list of recognised tokens,-||| and the line, column, and remainder of the input at the first point in the-||| string where there are no recognised tokens.-export-lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))-lex tmap str = let (ts, (l, c, str')) = tokenise 0 0 [] tmap (mkStr str) in-                   (ts, (l, c, getString str'))+    middle : Recognise False+    middle = manyUntil end (blockComment start end <|> any)

@@ -0,0 +1,193 @@+module Text.Lexer.Core++import Data.Bool.Extra++import public Control.Delayed++%default total++||| A language of token recognisers.+||| @ consumes If `True`, this recogniser is guaranteed to consume at+|||            least one character of input when it succeeds.+export+data Recognise : (consumes : Bool) -> Type where+     Empty : Recognise False+     Fail : Recognise c+     Lookahead : (positive : Bool) -> Recognise c -> Recognise False+     Pred : (Char -> Bool) -> Recognise True+     SeqEat : Recognise True -> Inf (Recognise e) -> Recognise True+     SeqEmpty : Recognise e1 -> Recognise e2 -> Recognise (e1 || e2)+     Alt : Recognise e1 -> Recognise e2 -> Recognise (e1 && e2)++||| A token recogniser. Guaranteed to consume at least one character.+public export+Lexer : Type+Lexer = Recognise True++||| Sequence two recognisers. If either consumes a character, the sequence+||| is guaranteed to consume a character.+export %inline+(<+>) : {c1 : Bool} ->+        Recognise c1 -> inf c1 (Recognise c2) -> Recognise (c1 || c2)+(<+>) {c1 = False} = SeqEmpty+(<+>) {c1 = True} = SeqEat++||| Alternative recognisers. If both consume, the combination is guaranteed+||| to consumer a character.+export+(<|>) : Recognise c1 -> Recognise c2 -> Recognise (c1 && c2)+(<|>) = Alt++||| A recogniser that always fails.+export+fail : Recognise c+fail = Fail++||| Recognise no input (doesn't consume any input)+export+empty : Recognise False+empty = Empty++||| Recognise a character that matches a predicate+export+pred : (Char -> Bool) -> Lexer+pred = Pred++||| Positive lookahead. Never consumes input.+export+expect : Recognise c -> Recognise False+expect = Lookahead True++||| Negative lookahead. Never consumes input.+export+reject : Recognise c -> Recognise False+reject = Lookahead False++||| Sequence the recognisers resulting from applying a function to each element+||| of a list. The resulting recogniser will consume input if the produced+||| recognisers consume and the list is non-empty.+export+concatMap : {c : Bool} ->+            (a -> Recognise c) -> (xs : List a) -> Recognise (c && isCons xs)+concatMap {c} _ [] = rewrite andFalseFalse c in Empty+concatMap {c} f (x :: xs) = rewrite andTrueNeutral c in+                            rewrite sym (orSameAndRightNeutral c (isCons xs)) in+                                    SeqEmpty (f x) (concatMap f xs)++data StrLen : Type where+     MkStrLen : String -> Nat -> StrLen++getString : StrLen -> String+getString (MkStrLen str n) = str++strIndex : StrLen -> Nat -> Maybe Char+strIndex (MkStrLen str len) i+    = if i >= len then Nothing+                  else Just (assert_total (prim__strIndex str (cast i)))++mkStr : String -> StrLen+mkStr str = MkStrLen str (length str)++strTail : Nat -> StrLen -> StrLen+strTail start (MkStrLen str len)+    = MkStrLen (substr start len str) (minus len start)++-- If the string is recognised, returns the index at which the token+-- ends+scan : Recognise c -> Nat -> StrLen -> Maybe Nat+scan Empty idx str = pure idx+scan Fail idx str = Nothing+scan (Lookahead positive r) idx str+    = if isJust (scan r idx str) == positive+         then Just idx+         else Nothing+scan (Pred f) idx str+    = do c <- strIndex str idx+         if f c+            then Just (idx + 1)+            else Nothing+scan (SeqEat r1 r2) idx str+    = do idx' <- scan r1 idx str+         -- TODO: Can we prove totality instead by showing idx has increased?+         assert_total (scan r2 idx' str)+scan (SeqEmpty r1 r2) idx str+    = do idx' <- scan r1 idx str+         scan r2 idx' str+scan (Alt r1 r2) idx str+    = case scan r1 idx str of+           Nothing => scan r2 idx str+           Just idx => Just idx++takeToken : Lexer -> StrLen -> Maybe (String, StrLen)+takeToken lex str+    = do i <- scan lex 0 str -- i must be > 0 if successful+         pure (substr 0 i (getString str), strTail i str)++||| A mapping from lexers to the tokens they produce.+||| This is a list of pairs `(Lexer, String -> tokenType)`+||| For each Lexer in the list, if a substring in the input matches, run+||| the associated function to produce a token of type `tokenType`+public export+TokenMap : (tokenType : Type) -> Type+TokenMap tokenType = List (Lexer, String -> tokenType)++||| A token, and the line and column where it was in the input+public export+record TokenData a where+  constructor MkToken+  line : Int+  col : Int+  tok : a++fspanEnd : Nat -> (Char -> Bool) -> String -> (Nat, String)+fspanEnd k p "" = (k, "")+fspanEnd k p xxs+    = assert_total $+      let x = prim__strHead xxs+          xs = prim__strTail xxs in+          if p x then fspanEnd (S k) p xs+                 else (k, xxs)++-- Faster version of 'span' from the prelude (avoids unpacking)+export+fspan : (Char -> Bool) -> String -> (String, String)+fspan p xs+    = let (end, rest) = fspanEnd 0 p xs in+          (substr 0 end xs, rest)++tokenise : (line : Int) -> (col : Int) ->+           List (TokenData a) -> TokenMap a ->+           StrLen -> (List (TokenData a), (Int, Int, StrLen))+tokenise line col acc tmap str+    = case getFirstToken tmap str of+           Just (tok, line', col', rest) =>+           -- assert total because getFirstToken must consume something+                assert_total (tokenise line' col' (tok :: acc) tmap rest)+           Nothing => (reverse acc, (line, col, str))+  where+    countNLs : List Char -> Nat+    countNLs str = List.length (filter (== '\n') str)++    getCols : String -> Int -> Int+    getCols x c+         = case fspan (/= '\n') (reverse x) of+                (incol, "") => c + cast (length incol)+                (incol, _) => cast (length incol)++    getFirstToken : TokenMap a -> StrLen -> Maybe (TokenData a, Int, Int, StrLen)+    getFirstToken [] str = Nothing+    getFirstToken ((lex, fn) :: ts) str+        = case takeToken lex str of+               Just (tok, rest) => Just (MkToken line col (fn tok),+                                         line + cast (countNLs (unpack tok)),+                                         getCols tok col, rest)+               Nothing => getFirstToken ts str++||| Given a mapping from lexers to token generating functions (the+||| TokenMap a) and an input string, return a list of recognised tokens,+||| and the line, column, and remainder of the input at the first point in the+||| string where there are no recognised tokens.+export+lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))+lex tmap str = let (ts, (l, c, str')) = tokenise 0 0 [] tmap (mkStr str) in+                   (ts, (l, c, getString str'))

@@ -0,0 +1,155 @@+||| A simple module to process 'literate' documents.+|||+||| The module uses a lexer to split the document into code blocks,+||| delineated by user-defined markers, and code lines that are+||| indicated be a line marker. The lexer returns a document stripped+||| of non-code elements but preserving the original document's line+||| count. Column numbering of code lines are not preserved.+|||+||| The underlying tokeniser is greedy.+|||+||| Once it identifies a line marker it reads a prettifying space then+||| consumes until the end of line. Once identifies a starting code+||| block marker, the lexer will consume input until the next+||| identifiable end block is encountered. Any other content is+||| treated as part of the original document.+|||+||| Thus, the input literate files *must* be well-formed w.r.t+||| to code line markers and code blocks.+|||+||| A further restriction is that literate documents cannot contain+||| the markers within the document's main text: This will confuse the+||| lexer.+|||+module Text.Literate++import Text.Lexer++import Data.List.Views++%default total++untilEOL : Recognise False+untilEOL = manyUntil (is '\n') any++line : String -> Lexer+line s = exact s <+> space <+> untilEOL++block : String -> String -> Lexer+block s e = exact s <+> manyUntil (exact e) any ++data Token = CodeBlock String String String+           | Any String+           | CodeLine String String++Show Token where+  showPrec d (CodeBlock l r x) = showCon d "CodeBlock" $ showArg l ++ showArg r ++ showArg x+  showPrec d (Any x)           = showCon d "Any" $ showArg x+  showPrec d (CodeLine m x)    = showCon d "CodeLine" $ showArg m ++ showArg x++rawTokens : (delims  : List (String, String))+         -> (markers : List String)+         -> TokenMap (Token)+rawTokens delims ls =+          map (\(l,r) => (block l r, CodeBlock l r)) delims+       ++ map (\m => (line m, CodeLine m)) ls+       ++ [(any, Any)]++||| Merge the tokens into a single source file.+reduce : List (TokenData Token) -> String -> String+reduce [] acc = acc+reduce (MkToken _ _ (Any x) :: rest) acc = reduce rest (acc ++ blank_content)+  where+    -- Preserve the original document's line count.+    blank_content : String+    blank_content = if elem '\n' (unpack x)+      then concat $ replicate (length (lines x)) "\n"+      else ""+reduce (MkToken _ _ (CodeLine m src) :: rest) acc =+    reduce rest (acc ++ (substr+                           (length m + 1) -- remove space to right of marker.+                           (length src)+                           src))++reduce (MkToken _ _ (CodeBlock l r src) :: rest) acc with (lines src) -- Strip the deliminators surrounding the block.+  reduce (MkToken _ _ (CodeBlock l r src) :: rest) acc | [] = reduce rest acc -- 1+  reduce (MkToken _ _ (CodeBlock l r src) :: rest) acc | (s :: ys) with (snocList ys)+    reduce (MkToken _ _ (CodeBlock l r src) :: rest) acc | (s :: []) | Empty = reduce rest acc -- 2+    reduce (MkToken _ _ (CodeBlock l r src) :: rest) acc | (s :: (srcs ++ [f])) | (Snoc rec) =+        reduce rest (acc ++ "\n" ++ unlines srcs ++ "\n")++-- [ NOTE ] 1 & 2 shouldn't happen as code blocks are well formed i.e. have two deliminators.+++public export+record LiterateError where+  constructor MkLitErr+  line   : Int+  column : Int+  input  : String++||| Description of literate styles.+|||+||| A 'literate' style comprises of+|||+||| + a list of code block deliminators (`deliminators`);+||| + a list of code line markers (`line_markers`); and+||| + a list of known file extensions `file_extensions`.+|||+||| Some example specifications:+|||+||| + Bird Style+|||+|||```+|||MkLitStyle Nil [">", "<"] Nil+|||```+|||+||| + Literate Haskell (for LaTeX)+|||+|||```+|||MkLitStyle [("\\begin{code}", "\\end{code}"),("\\begin{spec}","\\end{spec}")]+|||           Nil+|||           ["lhs", "tex"]+|||```+|||+||| + OrgMode+|||+|||```+|||MkLitStyle [("#+BEGIN_SRC idris","#+END_SRC"), ("#+COMMENT idris","#+END_COMMENT")]+|||           ["#+IDRIS:"]+|||           ["org"]+|||```+|||+public export+record LiterateStyle where+  constructor MkLitStyle+  ||| The pairs of start and end tags for code blocks.+  deliminators : List (String, String)++  ||| Line markers that indicate a line contains code.+  line_markers : List String++  ||| Recognised file extensions. Not used by the module, but will be+  ||| of use when connecting to code that reads in the original source+  ||| files.+  file_extensions : List String++||| Given a 'literate specification' extract the code from the+||| literate source file (`litStr`) that follows the presented style.+|||+||| @specification The literate specification to use.+||| @litStr  The literate source file.+|||+||| Returns a `LiterateError` if the literate file contains malformed+||| code blocks or code lines.+|||+export+extractCode : (specification : LiterateStyle)+           -> (litStr        : String)+           -> Either LiterateError String+extractCode (MkLitStyle delims markers exts) str =+      case lex (rawTokens delims markers) str of+        (toks, (_,_,"")) => Right $ reduce toks ""+        (_, (l,c,i))     => Left (MkLitErr l c i)++-- --------------------------------------------------------------------- [ EOF ]

@@ -1,270 +1,226 @@ module Text.Parser -%default total+import Data.Bool.Extra --- TODO: Add some primitives for helping with error messages.--- e.g. perhaps set a string to state what we're currently trying to--- parse, or to say what the next expected token is in words+import public Text.Parser.Core+import public Text.Quantity+import public Text.Token -||| Description of a language's grammar. The `tok` parameter is the type-||| of tokens, and the `consumes` flag is True if the language is guaranteed-||| to be non-empty - that is, successfully parsing the language is guaranteed-||| to consume some input.-export-data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where-     Empty : (val : ty) -> Grammar tok False ty-     Terminal : (tok -> Maybe a) -> Grammar tok True a-     NextIs : (tok -> Bool) -> Grammar tok False tok-     EOF : Grammar tok False ()+%access export+%default total -     Fail : String -> Grammar tok c ty-     Commit : Grammar tok False ()+||| Parse a terminal based on a kind of token.+match : (Eq k, TokenKind k) =>+        (kind : k) ->+        Grammar (Token k) True (TokType kind)+match kind = terminal $+  \(Tok kind' text) => if kind' == kind+                          then Just $ tokValue kind text+                          else Nothing -     SeqEat : Grammar tok True a -> Inf (a -> Grammar tok c2 b) ->-              Grammar tok True b-     SeqEmpty : {c1, c2 : Bool} ->-                Grammar tok c1 a -> (a -> Grammar tok c2 b) ->-                Grammar tok (c1 || c2) b-     Alt : {c1, c2 : Bool} ->-           Grammar tok c1 ty -> Grammar tok c2 ty ->-           Grammar tok (c1 && c2) ty+||| Optionally parse a thing, with a default value if the grammar doesn't+||| match. May match the empty input.+option : {c : Bool} ->+         (def : a) -> (p : Grammar tok c a) ->+         Grammar tok False a+option {c = False} def p = p <|> pure def+option {c = True} def p = p <|> pure def -public export-inf : Bool -> Type -> Type-inf True t = Inf t-inf False t = t+||| Optionally parse a thing.+||| To provide a default value, use `option` instead.+optional : (p : Grammar tok c a) ->+           Grammar tok False (Maybe a)+optional p = option Nothing (map Just p) -||| Sequence two grammars. If either consumes some input, the sequence is-||| guaranteed to consume some input. If the first one consumes input, the-||| second is allowed to be recursive (because it means some input has been-||| consumed and therefore the input is smaller)-export %inline-(>>=) : {c1 : Bool} ->-        Grammar tok c1 a -> inf c1 (a -> Grammar tok c2 b) ->-        Grammar tok (c1 || c2) b-(>>=) {c1 = False} = SeqEmpty-(>>=) {c1 = True} = SeqEat+||| Try to parse one thing or the other, producing a value that indicates+||| which option succeeded. If both would succeed, the left option+||| takes priority.+choose : (l : Grammar tok c1 a) ->+         (r : Grammar tok c2 b) ->+         Grammar tok (c1 && c2) (Either a b)+choose l r = map Left l <|> map Right r -||| Give two alternative grammars. If both consume, the combination is-||| guaranteed to consume.-export-(<|>) : Grammar tok c1 ty -> Grammar tok c2 ty ->-        Grammar tok (c1 && c2) ty-(<|>) = Alt+||| Produce a grammar by applying a function to each element of a container,+||| then try each resulting grammar until the first one succeeds. Fails if the+||| container is empty.+choiceMap : {c : Bool} ->+            (a -> Grammar tok c b) ->+            Foldable t => t a ->+            Grammar tok c b+choiceMap {c} f xs = foldr (\x, acc => rewrite sym (andSameNeutral c) in+                                               f x <|> acc)+                           (fail "No more options") xs -export-pure : (val : ty) -> Grammar tok False ty-pure = Empty+||| Try each grammar in a container until the first one succeeds.+||| Fails if the container is empty.+choice : Foldable t => t (Grammar tok c a) ->+         Grammar tok c a+choice = choiceMap id -||| Check whether the next token satisfies a predicate-export-nextIs : (tok -> Bool) -> Grammar tok False tok-nextIs = NextIs+mutual+  ||| Parse one or more things+  some : Grammar tok True a ->+         Grammar tok True (List a)+  some p = pure (!p :: !(many p)) -||| Look at the next token in the input-export-peek : Grammar tok False tok-peek = nextIs (const True)+  ||| Parse zero or more things (may match the empty input)+  many : Grammar tok True a ->+         Grammar tok False (List a)+  many p = option [] (some p) -||| Succeeds if running the predicate on the next token returns Just x,-||| returning x. Otherwise fails.-export-terminal : (tok -> Maybe a) -> Grammar tok True a-terminal = Terminal+||| Parse one or more instances of `p`, returning the parsed items and proof+||| that the resulting list is non-empty.+some' : (p : Grammar tok True a) ->+        Grammar tok True (xs : List a ** NonEmpty xs)+some' p = pure (!p :: !(many p) ** IsNonEmpty) -||| Always fail with a message-export-fail : String -> Grammar tok c ty-fail = Fail+mutual+  private+  count1 : (q : Quantity) ->+           (p : Grammar tok True a) ->+           Grammar tok True (List a)+  count1 q p = do x <- p+                  seq (count q p)+                      (\xs => pure (x :: xs)) -||| Succeed if the input is empty-export-eof : Grammar tok False ()-eof = EOF+  ||| Parse `p`, repeated as specified by `q`, returning the list of values.+  count : (q : Quantity) ->+          (p : Grammar tok True a) ->+          Grammar tok (isSucc (min q)) (List a)+  count (Qty Z Nothing) p = many p+  count (Qty Z (Just Z)) _ = pure []+  count (Qty Z (Just (S max))) p = option [] $ count1 (atMost max) p+  count (Qty (S min) Nothing) p = count1 (atLeast min) p+  count (Qty (S min) (Just Z)) _ = fail "Quantity out of order"+  count (Qty (S min) (Just (S max))) p = count1 (between (S min) max) p -||| Commit to an alternative; if the current branch of an alternative-||| fails to parse, no more branches will be tried-export-commit : Grammar tok False ()-commit = Commit+mutual+  ||| Parse one or more instances of `p` until `end` succeeds, returning the+  ||| list of values from `p`. Guaranteed to consume input.+  someTill : {c : Bool} ->+             (end : Grammar tok c e) ->+             (p : Grammar tok True a) ->+             Grammar tok True (List a)+  someTill {c} end p = do x <- p+                          seq (manyTill end p)+                              (\xs => pure (x :: xs)) -data ParseResult : List tok -> (consumes : Bool) -> Type -> Type where-     Failure : {xs : List tok} ->-               (committed : Bool) ->-               (err : String) -> (rest : List tok) -> ParseResult xs c ty-     EmptyRes : (committed : Bool) ->-                (val : ty) -> (more : List tok) -> ParseResult more False ty-     NonEmptyRes : (committed : Bool) ->-                   (val : ty) -> (more : List tok) ->-                   ParseResult (x :: xs ++ more) c ty+  ||| Parse zero or more instances of `p` until `end` succeeds, returning the+  ||| list of values from `p`. Guaranteed to consume input if `end` consumes.+  manyTill : {c : Bool} ->+             (end : Grammar tok c e) ->+             (p : Grammar tok True a) ->+             Grammar tok c (List a)+  manyTill {c} end p = rewrite sym (andTrueNeutral c) in+                               map (const []) end <|> someTill end p -weakenRes : {whatever, c : Bool} -> {xs : List tok} ->-            ParseResult xs c ty -> ParseResult xs (whatever && c) ty-weakenRes (Failure com msg ts) = Failure com msg ts-weakenRes {whatever=True} (EmptyRes com val xs) = EmptyRes com val xs-weakenRes {whatever=False} (EmptyRes com val xs) = EmptyRes com val xs-weakenRes (NonEmptyRes com val more) = NonEmptyRes com val more+||| Parse one or more instances of `p` until `end` succeeds, returning the+||| list of values from `p`, along with a proof that the resulting list is+||| non-empty.+someTill' : {c : Bool} ->+            (end : Grammar tok c a) ->+            (p : Grammar tok True a) ->+            Grammar tok True (xs : List a ** NonEmpty xs)+someTill' end p+  = do x <- p+       seq (manyTill end p)+           (\xs => pure (x :: xs ** IsNonEmpty)) -shorter : (more : List tok) -> .(ys : List tok) ->-          LTE (S (length more)) (S (length (ys ++ more)))-shorter more [] = lteRefl-shorter more (x :: xs) = LTESucc (lteSuccLeft (shorter more xs))+mutual+  ||| Parse one or more instance of `skip` until `p` is encountered,+  ||| returning its value.+  afterSome : (skip : Grammar tok True s) ->+              (p : Grammar tok c a) ->+              Grammar tok True a+  afterSome skip p = do skip+                        afterMany skip p -doParse : {c : Bool} ->-          (commit : Bool) -> (xs : List tok) -> (act : Grammar tok c ty) ->-          ParseResult xs c ty-doParse com xs act with (sizeAccessible xs)-  doParse com xs (Empty val) | sml = EmptyRes com val xs-  doParse com [] (Fail str) | sml = Failure com str []-  doParse com (x :: xs) (Fail str) | sml = Failure com str (x :: xs)-  doParse com xs Commit | sml = EmptyRes True () xs+  ||| Parse zero or more instance of `skip` until `p` is encountered,+  ||| returning its value.+  afterMany : {c : Bool} ->+              (skip : Grammar tok True s) ->+              (p : Grammar tok c a) ->+              Grammar tok c a+  afterMany {c} skip p = rewrite sym (andTrueNeutral c) in+                                 p <|> afterSome skip p -  doParse com [] (Terminal f) | sml = Failure com "End of input" []-  doParse com (x :: xs) (Terminal f) | sml-        = maybe-             (Failure com "Unrecognised token" (x :: xs))-             (\a => NonEmptyRes com {xs=[]} a xs)-             (f x)-  doParse com [] EOF | sml = EmptyRes com () []-  doParse com (x :: xs) EOF | sml-        = Failure com "Expected end of input" (x :: xs)-  doParse com [] (NextIs f) | sml = Failure com "End of input" []-  doParse com (x :: xs) (NextIs f) | sml-        = if f x-             then EmptyRes com x (x :: xs)-             else Failure com "Unrecognised token" (x :: xs)-  doParse com xs (Alt x y) | sml with (doParse False xs x | sml)-    doParse com xs (Alt x y) | sml | Failure com' msg ts-          = if com' -- If the alternative had committed, don't try the-                    -- other branch (and reset commit flag)-               then Failure com msg ts-               else weakenRes (doParse False xs y | sml)-    -- Successfully parsed the first option, so use the outer commit flag-    doParse com xs (Alt x y) | sml | (EmptyRes _ val xs)-          = EmptyRes com val xs-    doParse com (z :: (ys ++ more)) (Alt x y) | sml | (NonEmptyRes _ val more)-          = NonEmptyRes com val more-  doParse com xs (SeqEmpty act next) | (Access morerec)-          = case doParse com xs act | Access morerec of-                 Failure com msg ts => Failure com msg ts-                 EmptyRes com val xs =>-                       case doParse com xs (next val) | (Access morerec) of-                            Failure com' msg ts => Failure com' msg ts-                            EmptyRes com' val xs => EmptyRes com' val xs-                            NonEmptyRes com' val more => NonEmptyRes com' val more-                 NonEmptyRes {x} {xs=ys} com val more =>-                       case (doParse com more (next val) | morerec _ (shorter more ys)) of-                            Failure com' msg ts => Failure com' msg ts-                            EmptyRes com' val _ => NonEmptyRes com' val more-                            NonEmptyRes {x=x1} {xs=xs1} com' val more' =>-                                 rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in-                                         NonEmptyRes com' val more'-  doParse com xs (SeqEat act next) | sml with (doParse com xs act | sml)-    doParse com xs (SeqEat act next) | sml | Failure com' msg ts-         = Failure com' msg ts-    doParse com (x :: (ys ++ more)) (SeqEat act next) | (Access morerec) | (NonEmptyRes com' val more)-         = case doParse com' more (next val) | morerec _ (shorter more ys) of-                Failure com' msg ts => Failure com' msg ts-                EmptyRes com' val _ => NonEmptyRes com' val more-                NonEmptyRes {x=x1} {xs=xs1} com' val more' =>-                     rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in-                             NonEmptyRes com' val more'-  -- This next line is not strictly necessary, but it stops the coverage-  -- checker taking a really long time and eating lots of memory...-  doParse _ _ _ | sml = Failure True "Help the coverage checker!" []+||| Parse one or more things, each separated by another thing.+sepBy1 : {c : Bool} ->+         (sep : Grammar tok True s) ->+         (p : Grammar tok c a) ->+         Grammar tok c (List a)+sepBy1 {c} sep p = rewrite sym (orFalseNeutral c) in+                           [| p :: many (sep *> p) |] -public export-data ParseError tok = Error String (List tok)+||| Parse zero or more things, each separated by another thing. May+||| match the empty input.+sepBy : (sep : Grammar tok True s) ->+        (p : Grammar tok c a) ->+        Grammar tok False (List a)+sepBy sep p = option [] $ sepBy1 sep p -||| Parse a list of tokens according to the given grammar. If successful,-||| returns a pair of the parse result and the unparsed tokens (the remaining-||| input).-export-parse : (xs : List tok) -> (act : Grammar tok c ty) ->-        Either (ParseError tok) (ty, List tok)-parse xs act-    = case doParse False xs act of-           Failure _ msg ts => Left (Error msg ts)-           EmptyRes _ val rest => pure (val, rest)-           NonEmptyRes _ val rest => pure (val, rest)+||| Parse one or more instances of `p` separated by `sep`, returning the+||| parsed items and proof that the resulting list is non-empty.+sepBy1' : {c : Bool} ->+         (sep : Grammar tok True s) ->+         (p : Grammar tok c a) ->+         Grammar tok c (xs : List a ** NonEmpty xs)+sepBy1' {c} sep p+  = rewrite sym (orFalseNeutral c) in+            seq p (\x => do xs <- many (sep *> p)+                            pure (x :: xs ** IsNonEmpty)) -||| Parse one or more things-export-some : Grammar tok True a ->-       Grammar tok True (List a)-some p = do x <- p-            (do xs <- some p-                pure (x :: xs)) <|> pure [x]+||| Parse one or more instances of `p` separated by and optionally terminated by+||| `sep`.+sepEndBy1 : {c : Bool} ->+            (sep : Grammar tok True s) ->+            (p : Grammar tok c a) ->+            Grammar tok c (List a)+sepEndBy1 {c} sep p = rewrite sym (orFalseNeutral c) in+                              sepBy1 sep p <* optional sep -||| Parse zero or more things (may match the empty input)-export-many : Grammar tok True a ->-       Grammar tok False (List a)-many p = some p-     <|> pure []+||| Parse zero or more instances of `p`, separated by and optionally terminated+||| by `sep`. Will not match a separator by itself.+sepEndBy : (sep : Grammar tok True s) ->+           (p : Grammar tok c a) ->+           Grammar tok False (List a)+sepEndBy sep p = option [] $ sepEndBy1 sep p -||| Parse one or more things, separated by another thing-export-sepBy1 : Grammar tok True () -> Grammar tok True a ->+||| Parse zero or more instances of `p`, separated by and optionally terminated+||| by `sep`, returning the parsed items and a proof that the resulting list+||| is non-empty.+sepEndBy1' : {c : Bool} ->+             (sep : Grammar tok True s) ->+             (p : Grammar tok c a) ->+             Grammar tok c (xs : List a ** NonEmpty xs)+sepEndBy1' {c} sep p = rewrite sym (orFalseNeutral c) in+                               sepBy1' sep p <* optional sep++||| Parse one or more instances of `p`, separated and terminated by `sep`.+endBy1 : {c : Bool} ->+         (sep : Grammar tok True s) ->+         (p : Grammar tok c a) ->          Grammar tok True (List a)-sepBy1 sep p = do x <- p-                  (do sep-                      xs <- sepBy1 sep p-                      pure (x :: xs)) <|> pure [x]+endBy1 {c} sep p = some $ rewrite sym (orTrueTrue c) in+                                  p <* sep -||| Parse zero or more things, separated by another thing. May-||| match the empty input.-export-sepBy : Grammar tok True () -> Grammar tok True a ->+endBy : (sep : Grammar tok True s) ->+        (p : Grammar tok c a) ->         Grammar tok False (List a)-sepBy sep p = sepBy1 sep p <|> pure []--||| Optionally parse a thing, with a default value if the grammar doesn't-||| match. May match the empty input.-export-optional : Grammar tok True a -> (ifNothing : a) ->-           Grammar tok False a-optional p def = p <|> pure def+endBy sep p = option [] $ endBy1 sep p +||| Parse zero or more instances of `p`, separated and terminated by `sep`,+||| returning the parsed items and a proof that the resulting list is non-empty.+endBy1' : {c : Bool} ->+          (sep : Grammar tok True s) ->+          (p : Grammar tok c a) ->+          Grammar tok True (xs : List a ** NonEmpty xs)+endBy1' {c} sep p = some' $ rewrite sym (orTrueTrue c) in+                                    p <* sep  ||| Parse an instance of `p` that is between `left` and `right`.-export-between : (left  : Grammar tok True ())-       -> (right : Grammar tok True ())-       -> (p     : Grammar tok True a)-       -> Grammar tok True a-between left right contents = do-   left-   res <- contents-   right-   pure res--||| Parse one or more instances of `p` separated by `s`, returning the-||| parsed items and proof the resulting list is non-empty.-export-sepBy1' : (sep : Grammar tok True ())-       -> (p   : Grammar tok True a)-       -> Grammar tok True (xs : List a ** NonEmpty xs)-sepBy1' sep p-    = do x <- p-         (do sep-             xs <- sepBy1 sep p-             pure (x :: xs ** IsNonEmpty)) <|> pure ([x] ** IsNonEmpty)--||| Parse one or more instances of `p`, returning the parsed items and proof the resulting list is non-empty.-export-some' : (p : Grammar tok True a)-     -> Grammar tok True (xs : List a ** NonEmpty xs)-some' p = do-   x <- p-   (do xs <- some p-       pure (x::xs ** IsNonEmpty)) <|> pure ([x] ** IsNonEmpty)---||| Optionally parse a thing. If the grammar provides a default use `optional` instead.-export-maybe : Grammar tok True a-     -> Grammar tok False (Maybe a)-maybe p =-      (do res <- p; pure $ Just res)-  <|> pure Nothing+between : (left : Grammar tok True l) ->+          (right : Grammar tok True r) ->+          (p : Grammar tok c a) ->+          Grammar tok True a+between left right contents = left *> contents <* right

@@ -0,0 +1,265 @@+module Text.Parser.Core++import public Control.Delayed++%default total++-- TODO: Add some primitives for helping with error messages.+-- e.g. perhaps set a string to state what we're currently trying to+-- parse, or to say what the next expected token is in words++||| Description of a language's grammar. The `tok` parameter is the type+||| of tokens, and the `consumes` flag is True if the language is guaranteed+||| to be non-empty - that is, successfully parsing the language is guaranteed+||| to consume some input.+export+data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where+     Empty : (val : ty) -> Grammar tok False ty+     Terminal : (tok -> Maybe a) -> Grammar tok True a+     NextIs : (tok -> Bool) -> Grammar tok False tok+     EOF : Grammar tok False ()++     Fail : String -> Grammar tok c ty+     Commit : Grammar tok False ()++     SeqEat : Grammar tok True a -> Inf (a -> Grammar tok c2 b) ->+              Grammar tok True b+     SeqEmpty : {c1, c2 : Bool} ->+                Grammar tok c1 a -> (a -> Grammar tok c2 b) ->+                Grammar tok (c1 || c2) b+     Alt : {c1, c2 : Bool} ->+           Grammar tok c1 ty -> Grammar tok c2 ty ->+           Grammar tok (c1 && c2) ty++||| Sequence two grammars. If either consumes some input, the sequence is+||| guaranteed to consume some input. If the first one consumes input, the+||| second is allowed to be recursive (because it means some input has been+||| consumed and therefore the input is smaller)+export %inline+(>>=) : {c1 : Bool} ->+        Grammar tok c1 a ->+        inf c1 (a -> Grammar tok c2 b) ->+        Grammar tok (c1 || c2) b+(>>=) {c1 = False} = SeqEmpty+(>>=) {c1 = True} = SeqEat++||| Sequence two grammars. If either consumes some input, the sequence is+||| guaranteed to consume input. This is an explicitly non-infinite version+||| of `>>=`.+export+seq : Grammar tok c1 a ->+      (a -> Grammar tok c2 b) ->+      Grammar tok (c1 || c2) b+seq = SeqEmpty++||| Sequence a grammar followed by the grammar it returns.+export+join : {c1 : Bool} ->+       Grammar tok c1 (Grammar tok c2 a) ->+       Grammar tok (c1 || c2) a+join {c1 = False} p = SeqEmpty p id+join {c1 = True} p = SeqEat p id++||| Give two alternative grammars. If both consume, the combination is+||| guaranteed to consume.+export+(<|>) : Grammar tok c1 ty ->+        Grammar tok c2 ty ->+        Grammar tok (c1 && c2) ty+(<|>) = Alt++||| Allows the result of a grammar to be mapped to a different value.+export+Functor (Grammar tok c) where+  map f (Empty val)  = Empty (f val)+  map f (Fail msg)   = Fail msg+  map f (Terminal g) = Terminal (\t => map f (g t))+  map f (Alt x y)    = Alt (map f x) (map f y)+  map f (SeqEat act next)+      = SeqEat act (\val => map f (next val))+  map f (SeqEmpty act next)+      = SeqEmpty act (\val => map f (next val))+  -- The remaining constructors (NextIs, EOF, Commit) have a fixed type,+  -- so a sequence must be used.+  map {c = False} f p = SeqEmpty p (Empty . f)++||| Sequence a grammar with value type `a -> b` and a grammar+||| with value type `a`. If both succeed, apply the function+||| from the first grammar to the value from the second grammar.+||| Guaranteed to consume if either grammar consumes.+export+(<*>) : Grammar tok c1 (a -> b) ->+        Grammar tok c2 a ->+        Grammar tok (c1 || c2) b+(<*>) x y = SeqEmpty x (\f => map f y)++||| Sequence two grammars. If both succeed, use the value of the first one.+||| Guaranteed to consume if either grammar consumes.+export+(<*) : Grammar tok c1 a ->+       Grammar tok c2 b ->+       Grammar tok (c1 || c2) a+(<*) x y = map const x <*> y++||| Sequence two grammars. If both succeed, use the value of the second one.+||| Guaranteed to consume if either grammar consumes.+export+(*>) : Grammar tok c1 a ->+       Grammar tok c2 b ->+       Grammar tok (c1 || c2) b+(*>) x y = map (const id) x <*> y++||| Produce a grammar that can parse a different type of token by providing a+||| function converting the new token type into the original one.+export+mapToken : (a -> b) -> Grammar b c ty -> Grammar a c ty+mapToken f (Empty val) = Empty val+mapToken f (Terminal g) = Terminal (g . f)+mapToken f (NextIs g) = SeqEmpty (NextIs (g . f)) (Empty . f)+mapToken f EOF = EOF+mapToken f (Fail msg) = Fail msg+mapToken f Commit = Commit+mapToken f (SeqEat act next) = SeqEat (mapToken f act) (\x => mapToken f (next x))+mapToken f (SeqEmpty act next) = SeqEmpty (mapToken f act) (\x => mapToken f (next x))+mapToken f (Alt x y) = Alt (mapToken f x) (mapToken f y)++||| Always succeed with the given value.+export+pure : (val : ty) -> Grammar tok False ty+pure = Empty++||| Check whether the next token satisfies a predicate+export+nextIs : (tok -> Bool) -> Grammar tok False tok+nextIs = NextIs++||| Look at the next token in the input+export+peek : Grammar tok False tok+peek = nextIs (const True)++||| Succeeds if running the predicate on the next token returns Just x,+||| returning x. Otherwise fails.+export+terminal : (tok -> Maybe a) -> Grammar tok True a+terminal = Terminal++||| Always fail with a message+export+fail : String -> Grammar tok c ty+fail = Fail++||| Succeed if the input is empty+export+eof : Grammar tok False ()+eof = EOF++||| Commit to an alternative; if the current branch of an alternative+||| fails to parse, no more branches will be tried+export+commit : Grammar tok False ()+commit = Commit++data ParseResult : List tok -> (consumes : Bool) -> Type -> Type where+     Failure : {xs : List tok} ->+               (committed : Bool) ->+               (err : String) -> (rest : List tok) -> ParseResult xs c ty+     EmptyRes : (committed : Bool) ->+                (val : ty) -> (more : List tok) -> ParseResult more False ty+     NonEmptyRes : (committed : Bool) ->+                   (val : ty) -> (more : List tok) ->+                   ParseResult (x :: xs ++ more) c ty++-- Take the result of an alternative branch, reset the commit flag to+-- the commit flag from the outer alternative, and weaken the 'consumes'+-- flag to take both alternatives into account+weakenRes : {whatever, c : Bool} -> {xs : List tok} ->+            (com' : Bool) ->+						ParseResult xs c ty -> ParseResult xs (whatever && c) ty+weakenRes com' (Failure com msg ts) = Failure com' msg ts+weakenRes {whatever=True} com' (EmptyRes com val xs) = EmptyRes com' val xs+weakenRes {whatever=False} com' (EmptyRes com val xs) = EmptyRes com' val xs+weakenRes com' (NonEmptyRes com val more) = NonEmptyRes com' val more++shorter : (more : List tok) -> .(ys : List tok) ->+          LTE (S (length more)) (S (length (ys ++ more)))+shorter more [] = lteRefl+shorter more (x :: xs) = LTESucc (lteSuccLeft (shorter more xs))++doParse : {c : Bool} ->+          (commit : Bool) -> (xs : List tok) -> (act : Grammar tok c ty) ->+          ParseResult xs c ty+doParse com xs act with (sizeAccessible xs)+  doParse com xs (Empty val) | sml = EmptyRes com val xs+  doParse com [] (Fail str) | sml = Failure com str []+  doParse com (x :: xs) (Fail str) | sml = Failure com str (x :: xs)+  doParse com xs Commit | sml = EmptyRes True () xs++  doParse com [] (Terminal f) | sml = Failure com "End of input" []+  doParse com (x :: xs) (Terminal f) | sml+        = maybe+             (Failure com "Unrecognised token" (x :: xs))+             (\a => NonEmptyRes com {xs=[]} a xs)+             (f x)+  doParse com [] EOF | sml = EmptyRes com () []+  doParse com (x :: xs) EOF | sml+        = Failure com "Expected end of input" (x :: xs)+  doParse com [] (NextIs f) | sml = Failure com "End of input" []+  doParse com (x :: xs) (NextIs f) | sml+        = if f x+             then EmptyRes com x (x :: xs)+             else Failure com "Unrecognised token" (x :: xs)+  doParse com xs (Alt x y) | sml with (doParse False xs x | sml)+    doParse com xs (Alt x y) | sml | Failure com' msg ts+          = if com' -- If the alternative had committed, don't try the+                    -- other branch (and reset commit flag)+               then Failure com msg ts+               else weakenRes com (doParse False xs y | sml)+    -- Successfully parsed the first option, so use the outer commit flag+    doParse com xs (Alt x y) | sml | (EmptyRes _ val xs)+          = EmptyRes com val xs+    doParse com (z :: (ys ++ more)) (Alt x y) | sml | (NonEmptyRes _ val more)+          = NonEmptyRes com val more+  doParse com xs (SeqEmpty act next) | (Access morerec)+          = case doParse com xs act | Access morerec of+                 Failure com msg ts => Failure com msg ts+                 EmptyRes com val xs =>+                       case doParse com xs (next val) | (Access morerec) of+                            Failure com' msg ts => Failure com' msg ts+                            EmptyRes com' val xs => EmptyRes com' val xs+                            NonEmptyRes com' val more => NonEmptyRes com' val more+                 NonEmptyRes {x} {xs=ys} com val more =>+                       case (doParse com more (next val) | morerec _ (shorter more ys)) of+                            Failure com' msg ts => Failure com' msg ts+                            EmptyRes com' val _ => NonEmptyRes com' val more+                            NonEmptyRes {x=x1} {xs=xs1} com' val more' =>+                                 rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in+                                         NonEmptyRes com' val more'+  doParse com xs (SeqEat act next) | sml with (doParse com xs act | sml)+    doParse com xs (SeqEat act next) | sml | Failure com' msg ts+         = Failure com' msg ts+    doParse com (x :: (ys ++ more)) (SeqEat act next) | (Access morerec) | (NonEmptyRes com' val more)+         = case doParse com' more (next val) | morerec _ (shorter more ys) of+                Failure com' msg ts => Failure com' msg ts+                EmptyRes com' val _ => NonEmptyRes com' val more+                NonEmptyRes {x=x1} {xs=xs1} com' val more' =>+                     rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in+                             NonEmptyRes com' val more'+  -- This next line is not strictly necessary, but it stops the coverage+  -- checker taking a really long time and eating lots of memory...+  doParse _ _ _ | sml = Failure True "Help the coverage checker!" []++public export+data ParseError tok = Error String (List tok)++||| Parse a list of tokens according to the given grammar. If successful,+||| returns a pair of the parse result and the unparsed tokens (the remaining+||| input).+export+parse : (act : Grammar tok c ty) -> (xs : List tok) ->+        Either (ParseError tok) (ty, List tok)+parse act xs+    = case doParse False xs act of+           Failure _ msg ts => Left (Error msg ts)+           EmptyRes _ val rest => pure (val, rest)+           NonEmptyRes _ val rest => pure (val, rest)

@@ -16,7 +16,7 @@    Cat     : (x : Doc) -> (y : Doc) -> Doc   Nest    : (lvl : Int) -> (x : Doc) -> Doc-  Union   : (x : Doc) -> (y : Doc) -> Doc+  Union   : (x : Doc) -> (y : Lazy Doc) -> Doc    Column  : (f : Int -> Doc) -> Doc   Nesting : (f : Int -> Doc) -> Doc@@ -162,11 +162,12 @@     nicest : (lvl : Int)           -> (col : Int)           -> (x : PrettyDoc)-          -> (y : PrettyDoc)+          -> (y : Lazy PrettyDoc)           -> PrettyDoc     nicest n k x y =-      let width = min (w - k) (rwidth - k + n)-       in if fits width x then x else y+      if fits (min (w - k) (rwidth - k + n)) x+      then x+      else y      best : (lvl : Int)         -> (col : Int)

@@ -0,0 +1,38 @@+module Text.Quantity++%access public export+%default total++record Quantity where+  constructor Qty+  min : Nat+  max : Maybe Nat++Show Quantity where+  show (Qty Z Nothing) = "*"+  show (Qty Z (Just (S Z))) = "?"+  show (Qty (S Z) Nothing) = "+"+  show (Qty min max) = "{" ++ show min ++ showMax ++ "}"+    where+      showMax : String+      showMax = case max of+                     Nothing => ","+                     Just max' => if min == max'+                                     then ""+                                     else "," ++ show max'++between : Nat -> Nat -> Quantity+between min max = Qty min (Just max)++atLeast : Nat -> Quantity+atLeast min = Qty min Nothing++atMost : Nat -> Quantity+atMost max = Qty 0 (Just max)++exactly : Nat -> Quantity+exactly n = Qty n (Just n)++inOrder : Quantity -> Bool+inOrder (Qty min Nothing) = True+inOrder (Qty min (Just max)) = min <= max

@@ -0,0 +1,38 @@+module Text.Token++%access public export+%default total++||| For a type `kind`, specify a way of converting the recognised+||| string into a value.+|||+||| ```idris example+||| data SimpleKind = SKString | SKInt | SKComma+|||+||| TokenKind SimpleKind where+|||   TokType SKString = String+|||   TokType SKInt = Int+|||   TokType SKComma = ()+|||+|||   tokValue SKString x = x+|||   tokValue SKInt x = cast x+|||   tokValue SKComma x = ()+||| ```+interface TokenKind (k : Type) where+  ||| The type that a token of this kind converts to.+  TokType : k -> Type++  ||| Convert a recognised string into a value. The type is determined+  ||| by the kind of token.+  tokValue : (kind : k) -> String -> TokType kind++||| A token of a particular kind and the text that was recognised.+record Token k where+  constructor Tok+  kind : k+  text : String++||| Get the value of a `Token k`. The resulting type depends upon+||| the kind of token.+value : TokenKind k => (t : Token k) -> TokType (kind t)+value (Tok k x) = tokValue k x

@@ -1,40 +1,101 @@ package contrib  opts = "--nobasepkgs --partial-eval --total -i ../prelude -i ../base"-modules = CFFI, CFFI.Types, CFFI.Memory, -          Control.Algebra,-          Control.Algebra.Lattice, Control.Algebra.VectorSpace,-          Control.Algebra.NumericImplementations,-          Control.Isomorphism.Primitives,-          Control.Partial,-          Control.Pipeline,-          Control.ST, Control.ST.ImplicitCall, Control.ST.Exception,+modules = CFFI+        , CFFI.Memory+        , CFFI.Types -          Interfaces.Verified,+        , Control.Algebra+        , Control.Algebra.Lattice+        , Control.Algebra.NumericImplementations+        , Control.Algebra.VectorSpace -          Data.Fun, Data.Rel,-          Data.Hash,-          Data.Matrix, Data.Matrix.Algebraic, Data.Matrix.Numeric,-          Data.Nat.DivMod, Data.Nat.DivMod.IteratedSubtraction,-          Data.ZZ, Data.Sign,-          Data.BoundedList,-          Data.Heap,-          Data.SortedMap, Data.SortedSet,-          Data.CoList, Data.Storable,-	  Data.List.Zipper,+        , Control.Delayed+        , Control.Isomorphism.Primitives+        , Control.Monad.Syntax+        , Control.Partial+        , Control.Pipeline -          Decidable.Decidable, Decidable.Order,+        , Control.ST+        , Control.ST.Exception+        , Control.ST.ImplicitCall+        , Control.ST.Random+        , Control.ST.File -          Network.Cgi, Network.Socket.Data, Network.Socket.Raw, Network.Socket,+        , Data.Bool.Extra+        , Data.BoundedList+        , Data.CoList+        , Data.Combinators+        , Data.Combinators.Applicative+        , Data.Combinators.Arrow+        , Data.Fin.Extra+        , Data.Fuel+        , Data.Fun+        , Data.Hash+        , Data.Heap+        , Data.IOArray+        , Data.List.Zipper -          System.Concurrency.Process,+        , Data.Matrix+        , Data.Matrix.Algebraic+        , Data.Matrix.Numeric -          Text.Lexer, Text.Parser,+        , Data.Nat.Parity+        , Data.Nat.DivMod+        , Data.Nat.DivMod.IteratedSubtraction -          Text.PrettyPrint.WL,-          Text.PrettyPrint.WL.Core,-          Text.PrettyPrint.WL.Characters,-          Text.PrettyPrint.WL.Combinators,+        , Data.Pairs.Implicit+        , Data.Rel+        , Data.Sign+        , Data.SortedMap+        , Data.SortedSet+        , Data.Storable+        , Data.Stream.Extra+        , Data.String.Extra+        , Data.ZZ -          Data.Fin.Extra+        , Decidable.Decidable+        , Decidable.Order++        , Interfaces.Correlative+        , Interfaces.Verified++        , Language.JSON+        , Language.JSON.Data+        , Language.JSON.Lexer+        , Language.JSON.Parser+        , Language.JSON.String+        , Language.JSON.String.Lexer+        , Language.JSON.String.Parser+        , Language.JSON.String.Tokens+        , Language.JSON.Tokens++        , Network.Cgi+        , Network.Socket+        , Network.Socket.Data+        , Network.Socket.Raw++        , System.Concurrency.Process++        , Test.Unit.Display+        , Test.Unit.Runners+        , Test.Unit.Generic+        , Test.Unit.Assertions+        , Test.Unit++        , Text.Lexer+        , Text.Lexer.Core++        , Text.Literate++        , Text.Parser+        , Text.Parser.Core++        , Text.PrettyPrint.WL.Core+        , Text.PrettyPrint.WL.Combinators+        , Text.PrettyPrint.WL.Characters+        , Text.PrettyPrint.WL++        , Text.Quantity+        , Text.Token

@@ -58,15 +58,15 @@   cast {n} _ = n  implementation Show (LogLevel n) where-  show OFF        = "OFF"-  show TRACE      = "TRACE"-  show DEBUG      = "DEBUG"-  show INFO       = "INFO"-  show WARN       = "WARN"-  show FATAL      = "FATAL"-  show ERROR      = "ERROR"-  show ALL        = "ALL"-  show (CUSTOM n) = unwords ["CUSTOM", show n]+  showPrec d OFF        = "OFF"+  showPrec d TRACE      = "TRACE"+  showPrec d DEBUG      = "DEBUG"+  showPrec d INFO       = "INFO"+  showPrec d WARN       = "WARN"+  showPrec d FATAL      = "FATAL"+  showPrec d ERROR      = "ERROR"+  showPrec d ALL        = "ALL"+  showPrec d (CUSTOM n) = showCon d "CUSTOM" $ showArg n  implementation Eq (LogLevel n) where   (==) x y = lvlEq x y

@@ -303,15 +303,8 @@ toEff : .(xs' : List EFFECT) -> EffM m a xs (\v => xs') -> EffM m a xs (\v => xs') toEff xs' = id -infixl 2 <*>- pure : a -> EffM m a xs (\v => xs) pure = Value--return : a -> EffM m a xs (\v => xs)-return = pure--%deprecate Effects.return "Please use `pure`."  pureM : (val : a) -> EffM m a (xs val) xs pureM = Value

@@ -1,21 +1,23 @@ package effects -opts    = "--nobasepkgs --partial-eval --typeintype -i ../prelude -i ../base"+opts = "--nobasepkgs --partial-eval --typeintype -i ../prelude -i ../base"  modules = Effects-        , Effect.Default-        , Effect.Monad +        , Effect.Default         , Effect.Exception         , Effect.File-        , Effect.State++        , Effect.Logging.Category+        , Effect.Logging.Default+        , Effect.Logging.Level++        , Effect.Memory+        , Effect.Monad+        , Effect.Perf         , Effect.Random-        , Effect.StdIO         , Effect.Select-        , Effect.Memory+        , Effect.State+        , Effect.StdIO         , Effect.System         , Effect.Trans-        , Effect.Logging.Level-        , Effect.Logging.Default-        , Effect.Logging.Category-        , Effect.Perf

@@ -1,44 +0,0 @@-module Default--interface Default a where-    default : a--implementation Default Int where-    default = 0--implementation Default Integer where-    default = 0--implementation Default Double where-    default = 0--implementation Default Nat where-    default = 0--implementation Default Char where-    default = '\0'--implementation Default String where-    default = ""--implementation Default Bool where-    default = False--implementation Default () where-    default = ()--implementation (Default a, Default b) => Default (a, b) where-    default = (default, default)--implementation Default (Maybe a) where-    default = Nothing--implementation Default (List a) where-    default = []--implementation Default a => Default (Vect n a) where-    default = mkDef _ where-      mkDef : (n : Nat) -> Vect n a-      mkDef Z = []-      mkDef (S k) = default :: mkDef k-

@@ -1,41 +0,0 @@-module Effect.Exception--import Effects-import System-import Control.IOExcept--data Exception : Type -> Effect where-     Raise : a -> { () } Exception a b--implementation Handler (Exception a) Maybe where-     handle _ (Raise e) k = Nothing--implementation Handler (Exception a) List where-     handle _ (Raise e) k = []--implementation Show a => Handler (Exception a) IO where-     handle _ (Raise e) k = do printLn e-                               believe_me (exit 1)--implementation Handler (Exception a) (IOExcept a) where-     handle _ (Raise e) k = ioM (pure (Left e))--implementation Handler (Exception a) (Either a) where-     handle _ (Raise e) k = Left e--EXCEPTION : Type -> EFFECT-EXCEPTION t = MkEff () (Exception t)--raise : a -> { [EXCEPTION a ] } Eff m b-raise err = call $ Raise err--------- TODO: Catching exceptions mid program?--- probably need to invoke a new interpreter---- possibly add a 'handle' to the Eff language so that an alternative--- handler can be introduced mid interpretation?

@@ -1,128 +0,0 @@--- -------------------------------------------------------- [ Effectful FileIO ]-module Effect.File--import Effects-import Control.IOExcept---||| A Dependent type to describe File Handles. File handles are-||| parameterised with the current state of the file: Closed; Open for-||| reading; and Open for writing.-||| -||| @ m The file mode. -data OpenFile : (m : Mode) -> Type where-     FH : File -> OpenFile m--openOK : Mode -> Bool -> Type-openOK m True = OpenFile m-openOK m False = ()---- ------------------------------------------------------------ [ The Protocol ]--||| Here the protocol for resource access is defined as an effect.-||| The state transitions diagram for the protocol is as follows:-||| -|||     digraph G {-||| -|||       empty; read; write; // States-||| -|||       empty -> read [label="Open R"];-|||       read -> empty [label="Close"];-|||       read -> read [label="ReadLine"];-|||       read -> read [label="EOF"];-|||           -|||       empty -> write [label="Open W"];-|||       write -> empty [label="Close"];-|||       write -> write [label="WriteLine"];-||| -|||     }-data FileIO : Effect where-  ||| Open a file with the specified mode.-  ||| -  ||| Opening a file successful moves the state from 'empty' to the-  ||| specified mode. If not successful the state is still 'empty'.-  ||| -  ||| @ fname The file name to be opened.-  ||| @ m The file mode.-  Open : (fname: String)-         -> (m : Mode)-         -> {() ==> {res} if res-                             then OpenFile m-                             else ()} FileIO Bool--  ||| Close a file.-  ||| -  ||| Closing a file moves the state from Open to closed.-  Close : {OpenFile m ==> ()} FileIO () --  ||| Read a line from the file.-  ||| -  ||| Only files that are open for reading can be read.-  ReadLine : {OpenFile Read}  FileIO String -  -  ||| Write a line to a file.-  ||| -  ||| Only file that are open for writing can be written to.-  WriteLine : String -> {OpenFile Write} FileIO ()--  ||| End of file?-  ||| -  ||| Only files open for reading can be tested for EOF-  EOF : {OpenFile Read}  FileIO Bool---- ------------------------------------------------------------ [ The Handlers ]----- An implementation of the resource access protocol for the IO Context.-implementation Handler FileIO IO where-    handle () (Open fname m) k = do h <- openFile fname m-                                    valid <- validFile h-                                    if valid then k True (FH h) -                                             else k False ()-    handle (FH h) Close      k = do closeFile h-                                    k () ()-    handle (FH h) ReadLine        k = do str <- fread h-                                         k str (FH h)-    handle (FH h) (WriteLine str) k = do fwrite h str-                                         k () (FH h)-    handle (FH h) EOF             k = do e <- feof h-                                         k e (FH h)---- -------------------------------------------------------------- [ The Effect ]-FILE_IO : Type -> EFFECT-FILE_IO t = MkEff t FileIO---- ------------------------------------------------------------ [ The Bindings ]------ Bind the IO context handlers to functions. These functions will run--- in the IO context.-----||| Open a file with the specified mode.-||| -||| @ fname The file name to be opened.-||| @ m The file mode.-open : (fname : String)-       -> (m : Mode)-       -> { [FILE_IO ()] ==> [FILE_IO (if result-                                          then OpenFile m-                                          else ())] } Eff e Bool-open f m = call $ Open f m---||| Close a file.-close : { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff e ()-close = call $ Close--||| Read a line from the file.-readLine : { [FILE_IO (OpenFile Read)] } Eff e String -readLine = call $ ReadLine--||| Write a line to a file.-writeLine : String -> { [FILE_IO (OpenFile Write)] } Eff e ()-writeLine str = call $ WriteLine str--||| End of file?-eof : { [FILE_IO (OpenFile Read)] } Eff e Bool -eof = call $ EOF---- --------------------------------------------------------------------- [ EOF ]

@@ -1,175 +0,0 @@-module Effect.Memory--import Effects-import Control.IOExcept--%access public--abstract-data MemoryChunk : Nat -> Nat -> Type where-     CH : Ptr -> MemoryChunk size initialized--abstract-data RawMemory : Effect where-     Allocate   : (n : Nat) ->-                  RawMemory () () (\v => MemoryChunk n 0)-     Free       : RawMemory () (MemoryChunk n i) (\v => ())-     Initialize : Bits8 ->-                  (size : Nat) ->-                  so (i + size <= n) ->-                  RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (i + size))-     Peek       : (offset : Nat) ->-                  (size : Nat) ->-                  so (offset + size <= i) ->-                  RawMemory (Vect size Bits8)-                            (MemoryChunk n i) (\v => MemoryChunk n i) -     Poke       :  (offset : Nat) ->-                  (Vect size Bits8) ->-                  so (offset <= i && offset + size <= n) ->-                  RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (max i (offset + size))) -     Move       : (src : MemoryChunk src_size src_init) ->-                  (dst_offset : Nat) ->-                  (src_offset : Nat) ->-                  (size : Nat) ->-                  so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->-                  so (src_offset + size <= src_init) ->-                  RawMemory () (MemoryChunk dst_size dst_init)-                            (\v => MemoryChunk dst_size (max dst_init (dst_offset + size))) -     GetRawPtr  : RawMemory (MemoryChunk n i) (MemoryChunk n i) (\v => MemoryChunk n i) --private-do_malloc : Nat -> IOExcept String Ptr-do_malloc size with (fromInteger (cast size) == size)-  | True  = do ptr <- ioe_lift $ mkForeign (FFun "malloc" [FInt] FPtr) (fromInteger $ cast size)-               fail  <- ioe_lift $ nullPtr ptr-               if fail then ioe_fail "Cannot allocate memory"-               else pure ptr-  | False = ioe_fail "The target architecture does not support adressing enough memory"--private-do_memset : Ptr -> Nat -> Bits8 -> Nat -> IO ()-do_memset ptr offset c size-  = mkForeign (FFun "idris_memset" [FPtr, FInt, FByte, FInt] FUnit)-              ptr (fromInteger $ cast offset) c (fromInteger $ cast size)--private-do_free : Ptr -> IO ()-do_free ptr = mkForeign (FFun "free" [FPtr] FUnit) ptr--private-do_memmove : Ptr -> Ptr -> Nat -> Nat -> Nat -> IO ()-do_memmove dest src dest_offset src_offset size-  = mkForeign (FFun "idris_memmove" [FPtr, FPtr, FInt, FInt, FInt] FUnit)-              dest src (fromInteger $ cast dest_offset) (fromInteger $ cast src_offset) (fromInteger $ cast size)--private-do_peek : Ptr -> Nat -> (size : Nat) -> IO (Vect size Bits8)-do_peek _   _       Z = pure (Prelude.Vect.Nil)-do_peek ptr offset (S n)-  = do b <- mkForeign (FFun "idris_peek" [FPtr, FInt] FByte) ptr (fromInteger $ cast offset)-       bs <- do_peek ptr (S offset) n-       Prelude.Applicative.pure (Prelude.Vect.(::) b bs)--private-do_poke : Ptr -> Nat -> Vect size Bits8 -> IO ()-do_poke _   _      []     = pure ()-do_poke ptr offset (b::bs)-  = do mkForeign (FFun "idris_poke" [FPtr, FInt, FByte] FUnit) ptr (fromInteger $ cast offset) b-       do_poke ptr (S offset) bs--implementation Handler RawMemory (IOExcept String) where-  handle () (Allocate n) k-    = do ptr <- do_malloc n-         k () (CH ptr)-  handle {-{res = MemoryChunk _ offset}-} (CH ptr) (Initialize {i} c size _) k-    = ioe_lift (do_memset ptr i c size) $> k () (CH ptr)-  handle (CH ptr) (Free) k-    = ioe_lift (do_free ptr) $> k () ()-  handle (CH ptr) (Peek offset size _) k-    = do res <- ioe_lift (do_peek ptr offset size)-         k res (CH ptr)-  handle (CH ptr) (Poke offset content _) k-    = do ioe_lift (do_poke ptr offset content)-         k () (CH ptr)-  handle (CH dest_ptr) (Move (CH src_ptr) dest_offset src_offset size _ _) k-    = do ioe_lift (do_memmove dest_ptr src_ptr dest_offset src_offset size)-         k () (CH dest_ptr)-  handle chunk (GetRawPtr) k-    = k chunk chunk--RAW_MEMORY : Type -> EFFECT-RAW_MEMORY t = MkEff t RawMemory--allocate : (n : Nat) -> -           Eff m () [RAW_MEMORY ()] (\v => [RAW_MEMORY (MemoryChunk n 0)])-allocate size = call $ Allocate size--initialize : {i : Nat} ->-             {n : Nat} ->-             Bits8 ->-             (size : Nat) ->-             so (i + size <= n) ->-             Eff m () [RAW_MEMORY (MemoryChunk n i)] -                       (\v => [RAW_MEMORY (MemoryChunk n (i + size))])-initialize c size prf = call $ Initialize c size prf--free : Eff m () [RAW_MEMORY (MemoryChunk n i)] (\v => [RAW_MEMORY ()])-free = call Free--peek : {i : Nat} ->-       (offset : Nat) ->-       (size : Nat) ->-       so (offset + size <= i) ->-       { [RAW_MEMORY (MemoryChunk n i)] } Eff m (Vect size Bits8) -peek offset size prf = call $ Peek offset size prf--poke : {n : Nat} ->-       {i : Nat} ->-       (offset : Nat) ->-       Vect size Bits8 ->-       so (offset <= i && offset + size <= n) ->-       Eff m () [RAW_MEMORY (MemoryChunk n i)] -              (\v => [RAW_MEMORY (MemoryChunk n (max i (offset + size)))])-poke offset content prf = call $ Poke offset content prf--private-getRawPtr : { [RAW_MEMORY (MemoryChunk n i)] } Eff m (MemoryChunk n i) -getRawPtr = call $ GetRawPtr--private-move' : {dst_size : Nat} ->-        {dst_init : Nat} ->-        {src_init : Nat} ->-        (src_ptr : MemoryChunk src_size src_init) ->-        (dst_offset : Nat) ->-        (src_offset : Nat) ->-        (size : Nat) ->-        so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->-        so (src_offset + size <= src_init) ->-        Eff m () [RAW_MEMORY (MemoryChunk dst_size dst_init)]-               (\v => [RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))])-move' src_ptr dst_offset src_offset size dst_bounds src_bounds-  = call $ Move src_ptr dst_offset src_offset size dst_bounds src_bounds--data MoveDescriptor = Dst | Src--move : {dst_size : Nat} ->-       {dst_init : Nat} ->-       {src_size : Nat} ->-       {src_init : Nat} ->-       (dst_offset : Nat) ->-       (src_offset : Nat) ->-       (size : Nat) ->-       so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->-       so (src_offset + size <= src_init) ->-       Eff m ()-              [ Dst ::: RAW_MEMORY (MemoryChunk dst_size dst_init)-              , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)]-              (\v =>-                [ Dst ::: RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))-                , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)])-move dst_offset src_offset size dst_bounds src_bounds-  = do src_ptr <- Src :- getRawPtr-       Dst :- move' src_ptr dst_offset src_offset size dst_bounds src_bounds-       pure ()-

@@ -1,21 +0,0 @@-module Effect.Monad--import Effects---- Eff is a monad too, so we can happily use it in a monad transformer.--using (xs : List EFFECT, m : Type -> Type)-  implementation Functor (\a => EffM m a xs (\v => xs)) where-    map f prog = do t <- prog-                    value (f t)--  implementation Applicative (\a => EffM m a xs (\v => xs)) where-    pure = value-    (<*>) f a = do f' <- f-                   a' <- a-                   value (f' a')--  implementation Monad (\a => Eff m a xs (\v => xs)) where-    (>>=) = Effects.(>>=)--

@@ -1,47 +0,0 @@-module Effect.Random--import Effects--data Random : Effect where -     getRandom : { Integer } Random Integer -     setSeed   : Integer -> { Integer } Random () --using (m : Type -> Type)-  implementation Handler Random m where-     handle seed getRandom k-              = let seed' = assert_total ((1664525 * seed + 1013904223) `prim__sremBigInt` (pow 2 32)) in-                    k seed' seed'-     handle seed (setSeed n) k = k () n--RND : EFFECT-RND = MkEff Integer Random--||| Generates a random Integer in a given range-rndInt : Integer -> Integer -> { [RND] } Eff m Integer-rndInt lower upper = do v <- call $ getRandom-                        pure (v `prim__sremBigInt` (upper - lower) + lower)--||| Generate a random number in Fin (S `k`)-||| -||| Note that rndFin k takes values 0, 1, ..., k.-rndFin : (k : Nat) -> { [RND] } Eff m (Fin (S k))-rndFin k = do let v = assert_total $ !(call getRandom) `prim__sremBigInt` (cast (S k))-              pure (toFin v)- where toFin : Integer -> Fin (S k) -       toFin x = case integerToFin x (S k) of-                      Just v => v-                      Nothing => toFin (assert_smaller x (x - cast (S k)))--||| Select a random element from a vector-rndSelect' : Vect (S k) a -> { [RND] } Eff IO a-rndSelect' {k} xs = pure (Vect.index !(rndFin k)  xs)--||| Select a random element from a list, or Nothing if the list is empty-rndSelect : List a -> { [RND] } Eff IO (Maybe a)-rndSelect []      = pure Nothing-rndSelect (x::xs) = pure (Just !(rndSelect' (x::(fromList xs))))--||| Sets the random seed-srand : Integer -> { [RND] } Eff m ()-srand n = call $ setSeed n-

@@ -1,23 +0,0 @@-module Effect.Select--import Effects--data Selection : Effect where-     Select : List a -> { () } Selection a --implementation Handler Selection Maybe where-     handle _ (Select xs) k = tryAll xs where-         tryAll [] = Nothing-         tryAll (x :: xs) = case k x () of-                                 Nothing => tryAll xs-                                 Just v => Just v--implementation Handler Selection List where-     handle r (Select xs) k = concatMap (\x => k x r) xs--SELECT : EFFECT-SELECT = MkEff () Selection--select : List a -> { [SELECT] } Eff m a -select xs = call $ Select xs-

@@ -1,40 +0,0 @@-module Effect.State--import Effects--%access public--data State : Effect where-  Get :      { a }       State a-  Put : b -> { a ==> b } State () --using (m : Type -> Type)-  implementation Handler State m where-     handle st Get     k = k st st-     handle st (Put n) k = k () n--STATE : Type -> EFFECT-STATE t = MkEff t State--get : { [STATE x] } Eff m x-get = call $ Get--put : x -> { [STATE x] } Eff m () -put val = call $ Put val--putM : y -> { [STATE x] ==> [STATE y] } Eff m () -putM val = call $ Put val--update : (x -> x) -> { [STATE x] } Eff m () -update f = put (f !get)--updateM : (x -> y) -> { [STATE x] ==> [STATE y] } Eff m () -updateM f = putM (f !get)--locally : x -> ({ [STATE x] } Eff m t) -> { [STATE y] } Eff m t -locally newst prog = do st <- get-                        putM newst-                        val <- prog-                        putM st-                        pure val-

@@ -1,60 +0,0 @@-module Effect.StdIO--import Effects-import Control.IOExcept------------------------------------------------------------------ IO effects internals----------------------------------------------------------------||| The internal representation of StdIO effects-data StdIO : Effect where-     PutStr : String -> { () } StdIO () -     GetStr : { () } StdIO String -     PutCh : Char -> { () } StdIO ()-     GetCh : { () } StdIO Char------------------------------------------------------------------- IO effects handlers----------------------------------------------------------------implementation Handler StdIO IO where-    handle () (PutStr s) k = do putStr s; k () ()-    handle () GetStr     k = do x <- getLine; k x ()-    handle () (PutCh c)  k = do putChar c; k () () -    handle () GetCh      k = do x <- getChar; k x ()--implementation Handler StdIO (IOExcept a) where-    handle () (PutStr s) k = do ioe_lift $ putStr s; k () ()-    handle () GetStr     k = do x <- ioe_lift $ getLine; k x ()-    handle () (PutCh c)  k = do ioe_lift $ putChar c; k () () -    handle () GetCh      k = do x <- ioe_lift $ getChar; k x ()------------------------------------------------------------------- The Effect and associated functions----------------------------------------------------------------STDIO : EFFECT-STDIO = MkEff () StdIO--||| Write a string to standard output.-putStr : String -> { [STDIO] } Eff e ()-putStr s = call $ PutStr s--||| Write a character to standard output.-putChar : Char -> { [STDIO] } Eff e ()-putChar c = call $ PutCh c--||| Write a string to standard output, terminating with a newline.-putStrLn : String -> { [STDIO] } Eff e ()-putStrLn s = putStr (s ++ "\n")--||| Read a string from standard input.-getStr : { [STDIO] } Eff e String-getStr = call $ GetStr--||| Read a character from standard input.-getChar : { [STDIO] } Eff e Char-getChar = call $ GetCh-