on master help sign in
Merge branch 'master' of Idris-dev into issue3796
commitab65a300fbde334a83480710170fbe6552f62139 authorEdmund Smith <edmund.pd.smith@gmail.com> dateTue 1 Aug 2017, 20:09 (9 years ago) parent5aaa39eb3df850
140 files changed+2445−745
.travis.yml+4−14 CHANGELOG.md+31−2 README.md+1−1 Setup.hs+1−16 appveyor.yml+1−1 codegen/idris-codegen-c/Main.hs+1 codegen/idris-codegen-javascript/Main.hs+1 codegen/idris-codegen-node/Main.hs+1 docs/reference/codegen.rst+10−10 docs/reference/elaborator-reflection.rst+6−1 docs/reference/ide-protocol.rst+10−10 docs/reference/syntax-guide.rst+8−2 docs/st/composing.rst+1−1 docs/tutorial/interfaces.rst+2−2 docs/tutorial/miscellany.rst+9 idris.cabal+16−38 libs/base/Control/Catchable.idr+22 libs/base/Control/Monad/RWS.idr+7−1 libs/base/Data/List/Views.idr+17−21 libs/base/Data/Nat/Views.idr+9−13 libs/base/Data/Vect/Views.idr+10−10 libs/contrib/Data/Heap.idr−4 libs/contrib/Data/SortedMap.idr+52−1 libs/contrib/Data/SortedSet.idr+4 libs/contrib/Text/Lexer.idr+238 libs/contrib/Text/Parser.idr+229 libs/contrib/Text/PrettyPrint/WL.idr+18 libs/contrib/Text/PrettyPrint/WL/Characters.idr+103 libs/contrib/Text/PrettyPrint/WL/Combinators.idr+259 libs/contrib/Text/PrettyPrint/WL/Core.idr+225 libs/contrib/contrib.ipkg+7 libs/prelude/Decidable/Equality.idr+15−9 libs/prelude/Prelude/Bool.idr+9 libs/prelude/Prelude/Cast.idr+1−1 libs/prelude/Prelude/Doubles.idr+3 libs/prelude/Prelude/List.idr+5−1 libs/prelude/Prelude/Monad.idr+6−1 libs/prelude/Prelude/Nat.idr+2−5 libs/prelude/Prelude/WellFounded.idr+40−22 main/Main.hs+1 rts/idris_gc.c+1−1 rts/idris_gmp.h+2 rts/idris_main.c+1 rts/idris_rts.c+86−42 rts/idris_rts.h+20−3 scripts/runidris+18 scripts/runidris-node+18 src/IRTS/CodegenC.hs+253−134 src/IRTS/Compiler.hs+2−1 src/IRTS/Defunctionalise.hs+1−1 src/IRTS/JavaScript/AST.hs+8−19 src/IRTS/JavaScript/Codegen.hs+11−2 src/IRTS/JavaScript/LangTransforms.hs+13 src/IRTS/JavaScript/PrimOp.hs+11−3 src/IRTS/Lang.hs+2−1 src/IRTS/Portable.hs+1−1 src/IRTS/Simplified.hs+1 src/Idris/ASTUtils.hs+1 src/Idris/AbsSyntax.hs+3−124 src/Idris/AbsSyntaxTree.hs+13−134 src/Idris/Apropos.hs+1 src/Idris/CaseSplit.hs+1−1 src/Idris/Chaser.hs+2 src/Idris/CmdOptions.hs+1−6 src/Idris/Core/Binary.hs+2 src/Idris/Core/CaseTree.hs+2−2 src/Idris/Core/DeepSeq.hs+4−1 src/Idris/Core/ProofState.hs+2−1 src/Idris/Core/TT.hs+4−2 src/Idris/Core/Typecheck.hs+2−2 src/Idris/Core/Unify.hs+1−1 src/Idris/Core/WHNF.hs+1−1 src/Idris/Coverage.hs+1−1 src/Idris/DSL.hs+2 src/Idris/DataOpts.hs+1−1 src/Idris/DeepSeq.hs+1 src/Idris/Docs.hs+2−1 src/Idris/Docstrings.hs+2−1 src/Idris/Elab/Clause.hs+1 src/Idris/Elab/Provider.hs+1 src/Idris/Elab/Quasiquote.hs+1 src/Idris/Elab/Term.hs+5−2 src/Idris/Elab/Type.hs+1 src/Idris/Elab/Utils.hs+7−6 src/Idris/ElabDecls.hs+1 src/Idris/Erasure.hs+1 src/Idris/Error.hs+1 src/Idris/IBC.hs+9−1 src/Idris/IdrisDoc.hs+2 src/Idris/Info.hs+1−1 src/Idris/Interactive.hs+14−16 src/Idris/Main.hs+1 src/Idris/ModeCommon.hs+1 src/Idris/Options.hs+283 src/Idris/Output.hs+2 src/Idris/Package.hs+1−1 src/Idris/Package/Common.hs+1−1 src/Idris/Package/Parser.hs+17−13 src/Idris/Parser.hs+8−2 src/Idris/Parser/Data.hs+1 src/Idris/Parser/Expr.hs+8 src/Idris/Parser/Helpers.hs+4−9 src/Idris/Parser/Ops.hs+2−1 src/Idris/PartialEval.hs+1−1 src/Idris/Prover.hs+2 src/Idris/REPL.hs+2−1 src/Idris/REPL/Commands.hs+1 src/Idris/REPL/Parser.hs+1 src/Idris/Reflection.hs−5 src/Idris/Termination.hs+1 src/Util/Pretty.hs+3 src/Util/System.hs+10 stack-shell.nix+1−1 stack.yaml+1−1 test/TestData.hs+5−2 test/TestRun.hs−2 test/basic009/expected+1−1 test/basic018/expected+4−2 test/interactive015/expected+6 test/interactive015/input+2 test/interactive015/run+8 test/interactive015/src/interactive015.idr+4 test/interactive016/expected+7 test/interactive016/input+2 test/interactive016/run+8 test/interactive016/src/interactive016.idr+7 test/interactive017/TestMod.idr+5 test/interactive017/expected+7 test/interactive017/run+9 test/interactive017/shebang-args.idr+6 test/interactive017/shebang-import.idr+6 test/interactive017/shebang-node.idr+4 test/interactive017/shebang.idr+4 test/pkg001/expected+3 test/pkg001/run+3 test/proof002/Reflect.idr+1−1 test/regression002/expected+2−1 test/regression003/expected+1 test/regression003/regression003.idr+56 test/regression003/run+4
.travis.yml+4−14
@@ -1,3 +1,4 @@
1+dist: trusty
12sudo: false
23
34language: c
@@ -10,15 +11,6 @@ matrix:
1011 include:
1112 - env: CABALVER="1.24" GHCVER="8.0.1" STACKVER="7.14" STYLISH=YES
1213 addons: {apt: {packages: [cabal-install-1.24,ghc-8.0.1,hscolour], sources: [hvr-ghc]}}
13− - os: osx
14− env: CABALVER="1.24" GHCVER="8.0.1" TESTS="test_c"
15− compiler: ": #GHC 8.0.1"
16− - env: CABALVER="1.20" GHCVER="7.6.3" TESTS="test_c"
17− compiler: ": #GHC 7.6.3"
18− addons: {apt: {packages: [cabal-install-1.20,ghc-7.6.3,cppcheck,hscolour], sources: [hvr-ghc]}}
19− - env: CABALVER="1.20" GHCVER="7.8.4" TESTS="test_c"
20− compiler: ": #GHC 7.8.4"
21− addons: {apt: {packages: [cabal-install-1.20,ghc-7.8.4,cppcheck,hscolour], sources: [hvr-ghc]}}
2214 - env: CABALVER="1.22" GHCVER="7.10.3" TESTS="lib_doc doc"
2315 compiler: ": #GHC 7.10.3"
2416 addons: {apt: {packages: [cabal-install-1.22,ghc-7.10.3,cppcheck,hscolour], sources: [hvr-ghc]}}
@@ -37,10 +29,6 @@ matrix:
3729 - env: CABALVER="1.24" GHCVER="8.0.1" TESTS="test_c"
3830 compiler: ": #GHC 8.0.1"
3931 addons: {apt: {packages: [cabal-install-1.24,ghc-8.0.1,cppcheck,hscolour], sources: [hvr-ghc]}}
40− allow_failures:
41− - os: osx
42− env: CABALVER="1.24" GHCVER="8.0.1" TESTS="test_c"
43− compiler: ": #GHC 8.0.1"
4432 fast-finish: true
4533
4634cache:
@@ -153,7 +141,9 @@ script:
153141 - echo -en 'travis_fold:end:script.tests\\r'
154142###
155143 - echo 'Benchmarks...' && echo -en 'travis_fold:start:script.benchmarks\\r'
156− - cd benchmarks && ./build.pl && ./run.pl && cd ..
144+ - if [[ "$TESTS" == "test_c" ]]; then
145+ cd benchmarks && ./build.pl && ./run.pl && cd ..;
146+ fi
157147 - echo -en 'travis_fold:end:script.benchmarks\\r'
158148###
159149# EOF
CHANGELOG.md+31−2
@@ -1,11 +1,40 @@
1+# New in 1.1.0
2+
3+## Library Updates
4+
5++ Added `Text.PrettyPrint.WL` an implementation of the Wadler-Leijen
6+ Pretty-Print algorithm. Useful for those wishing to pretty print
7+ things.
8++ Added `Text.Lexer` and `Text.Parser` to `contrib`. These are small libraries
9+ for implementing total lexical analysers and parsers.
10++ New instances:
11+ + Added `Catchable` for `ReaderT`, `WriterT`, and `RWST`.
12+ + Added `MonadTrans` for `RWST`.
13++ Added utility functions to `Data.SortedMap` and `Data.SortedSet` (`contrib`),
14+ most notably `merge`, merging two maps by their `Semigroup` op (`<+>`)
15++ `Prelude.WellFounded` now contains an interface `Sized a` that defines a size
16+ mapping from `a` to `Nat`. For example, there is an implementation for lists,
17+ where `size = length`.
18+
19+ The function `sizeAccessible` then proves well-foundedness of the relation
20+ `Smaller x y = LT (size x) (size y)`, which allows us to use strong
21+ induction conveniently with any type that implements `Sized`.
22+
23+ In practice, this allows us to write functions that recurse not only on
24+ direct subterms of their arguments but on any value
25+ with a (strictly) smaller `size`.
26+
27+ A good example of this idiom at work is `Data.List.Views.splitRec` from `base`.
28++ Added utility lemma `decEqSelfIsYes : decEq x x = Yes Refl` to
29+ `Decidable.Equality`. This is primarily useful for proving properties of
30+ functions defined with the help of `decEq`.
131
232## Tool Updates
333
434+ New JavaScript code generator that uses an higher level intermediate
535 representation.
636
7−+ Various optimizations of the novel JavaScript code generator to make
8− its results fast.
37++ Various optimizations of the new JavaScript code generator.
938
1039+ Names are now annotated with their representations over the IDE
1140 protocol, which allows IDEs to provide commands that work on special
README.md+1−1
@@ -3,7 +3,7 @@
33[![Build Status](https://travis-ci.org/idris-lang/Idris-dev.svg?branch=master)](https://travis-ci.org/idris-lang/Idris-dev)
44[![Appveyor build](https://ci.appveyor.com/api/projects/status/xi8yu81oy1134g7o/branch/master?svg=true)](https://ci.appveyor.com/project/idrislang/idris-dev)
55[![Documentation Status](https://readthedocs.org/projects/idris/badge/?version=latest)](https://readthedocs.org/projects/idris/?badge=latest)
6−[![Hackage](https://budueba.com/hackage/idris)](https://hackage.haskell.org/package/idris)
6+[![Hackage](https://img.shields.io/hackage/v/idris.svg)](https://hackage.haskell.org/package/idris)
77[![Stackage LTS](http://stackage.org/package/idris/badge/lts)](http://stackage.org/lts/package/idris)
88[![Stackage Nightly](http://stackage.org/package/idris/badge/nightly)](http://stackage.org/nightly/package/idris)
99[![IRC](https://img.shields.io/badge/IRC-%23idris-1e72ff.svg?style=flat)](https://www.irccloud.com/invite?channel=%23idris&hostname=irc.freenode.net&port=6697&ssl=1)
Setup.hs+1−16
@@ -274,26 +274,15 @@ idrisInstall verbosity copy pkg local = unless (execOnly (configFlags local)) $
274274-- -----------------------------------------------------------------------------
275275-- Test
276276
277−-- FIXME: We use the __GLASGOW_HASKELL__ macro because MIN_VERSION_cabal seems
278−-- to be broken !
279−
280277-- There are two "dataDir" in cabal, and they don't relate to each other.
281278-- When fetching modules, idris uses the second path (in the pkg record),
282279-- which by default is the root folder of the project.
283280-- We want it to be the install directory where we put the idris libraries.
284281fixPkg pkg target = pkg { dataDir = target }
285282
286−-- The "Args" argument of the testHooks has been added in cabal 1.22.0,
287−-- and should therefore be ignored for prior versions.
288−#if __GLASGOW_HASKELL__ < 710
289−originalTestHook _ = testHook simpleUserHooks
290−#else
291−originalTestHook = testHook simpleUserHooks
292−#endif
293−
294283idrisTestHook args pkg local hooks flags = do
295284 let target = datadir $ L.absoluteInstallDirs pkg local NoCopyDest
296− originalTestHook args (fixPkg pkg target) local hooks flags
285+ testHook simpleUserHooks args (fixPkg pkg target) local hooks flags
297286
298287-- -----------------------------------------------------------------------------
299288-- Main
@@ -314,9 +303,5 @@ main = defaultMainWithHooks $ simpleUserHooks
314303 , preSDist = idrisPreSDist
315304 , sDistHook = idrisSDist (sDistHook simpleUserHooks)
316305 , postSDist = idrisPostSDist
317−#if __GLASGOW_HASKELL__ < 710
318− , testHook = idrisTestHook ()
319−#else
320306 , testHook = idrisTestHook
321−#endif
322307 }
appveyor.yml+1−1
@@ -1,7 +1,7 @@
11version: 1.0.{build}
22init:
33- ps: >-
4− choco install cabal
4+ choco install cabal --no-progress
55
66 mkdir C:\ghc
77
codegen/idris-codegen-c/Main.hs+1
@@ -4,6 +4,7 @@ import Idris.AbsSyntax
44import Idris.Core.TT
55import Idris.ElabDecls
66import Idris.Main
7+import Idris.Options
78import IRTS.CodegenC
89import IRTS.Compiler
910
codegen/idris-codegen-javascript/Main.hs+1
@@ -4,6 +4,7 @@ import Idris.AbsSyntax
44import Idris.Core.TT
55import Idris.ElabDecls
66import Idris.Main
7+import Idris.Options
78import IRTS.CodegenJavaScript
89import IRTS.Compiler
910
codegen/idris-codegen-node/Main.hs+1
@@ -4,6 +4,7 @@ import Idris.AbsSyntax
44import Idris.Core.TT
55import Idris.ElabDecls
66import Idris.Main
7+import Idris.Options
78import IRTS.CodegenJavaScript
89import IRTS.Compiler
910
docs/reference/codegen.rst+10−10
@@ -27,16 +27,6 @@ issue the following command:
2727 $ idris --codegen javascript hello.idr -o hello.js
2828
2929
30−Generating code for NodeJS is slightly different. Idris outputs a
31−JavaScript file that can be directly executed via node.
32−
33−::
34−
35− $ idris --codegen node hello.idr -o hello
36− $ ./hello
37− Hello world
38−
39−
4030Idris can produce very big chunks of JavaScript code (hello world
4131weighs in at 1500 lines). However, the generated code can be minified
4232using the `closure-compiler
@@ -50,6 +40,16 @@ using the `closure-compiler
5040Node.js
5141-------
5242
43+Generating code for NodeJS is slightly different. Idris outputs a
44+JavaScript file that can be directly executed via node.
45+
46+::
47+
48+ $ idris --codegen node hello.idr -o hello
49+ $ ./hello
50+ Hello world
51+
52+
5353
5454Third Party
5555============
docs/reference/elaborator-reflection.rst+6−1
@@ -32,6 +32,9 @@ Running Elaborator Scripts
3232
3333On their own, tactics have no effect.
3434The meta-operation ``%runElab script`` runs ``script`` in the current elaboration context.
35+Before you can use ``%runElab``, you will have to enable the language extension by adding
36+``%language ElabReflection`` in your file (or by passing ``-X ElabReflection`` to the
37+``idris`` executable from your command line).
3538For example, the following script constructs the identity function at type ``Nat``:
3639
3740.. code-block:: idris
@@ -88,7 +91,9 @@ that fills the hole.
8891
8992The interactive elaboration shell accepts a limited number of commands,
9093including a subset of the commands understood by the normal Idris REPL
91−as well as some elaboration-specific commands.
94+as well as some elaboration-specific commands. It also supports the
95+``do``-syntax, meaning you can write ``res <- command`` to bind the result of
96+``command`` to variable ``res``.
9297
9398General-purpose commands:
9499
docs/reference/ide-protocol.rst+10−10
@@ -45,15 +45,12 @@ This is achieved by the already seen ``:load-file`` command.
4545
4646The available commands include:
4747
48− ``(:load-file FILENAME)``
49− Load the named file.
48+ ``(:load-file FILENAME [LINE])``
49+ Load the named file. If a ``LINE`` number is provided, the file is only loaded up to that line. Otherwise, the entire file is loaded.
5050
5151 ``(:interpret STRING)``
5252 Interpret ``STRING`` at the Idris REPL, returning a highlighted result.
5353
54− ``(:repl-completions STRING)``
55− Return the result of tab-completing ``STRING`` as a REPL command.
56−
5754 ``(:type-of STRING)``
5855 Return the type of the name, written with Idris syntax in the ``STRING``.
5956 The reply may contain highlighting information.
@@ -88,9 +85,12 @@ The available commands include:
8885 Attempt to fill out the holes on ``LINE`` named ``NAME`` by proof search.
8986 ``HINTS`` is a possibly-empty list of additional things to try while searching.
9087
91− ``(:docs-for NAME)``
92− Look up the documentation for ``NAME``, and return it as a highlighted string.
93−
88+ ``(:docs-for NAME [MODE])``
89+ Look up the documentation for ``NAME``, and return it as a highlighted string. If ``MODE`` is ``:overview``, only the first paragraph of documentation is provided for ``NAME``. If ``MODE`` is ``:full``, or omitted, the full documentation is returned for ``NAME``.
90+
91+ ``(:apropos STRING)``
92+ Search the documentation for mentions of ``STRING``, and return any found as a list of highlighted strings.
93+
9494 ``(:metavariables WIDTH)``
9595 List the currently-active holes, with their types pretty-printed with ``WIDTH`` columns.
9696
@@ -119,9 +119,9 @@ The available commands include:
119119 Return the definition of ``NAME`` as a highlighted string.
120120
121121 ``(:repl-completions NAME)``
122− Search names, types and documentations which contain ``NAME``.
122+ Search names, types and documentations which contain ``NAME``. Return the result of tab-completing ``NAME`` as a REPL command.
123123
124− ``(:version UID)``
124+ ``:version``
125125 Return the version information of the Idris compiler.
126126
127127
docs/reference/syntax-guide.rst+8−2
@@ -223,7 +223,7 @@ Every occurence of the the defined type in a constructor argument will be
223223wrapped in the ``Inf`` type constructor. This has the effect of delaying the
224224evaluation of the second argument when the data constructor is applied.
225225An ``Inf`` argument is constructed using ``Delay`` (which Idris will insert
226−implicitly) adn evaluated using ``Force`` (again inserted implicitly).
226+implicitly) and evaluated using ``Force`` (again inserted implicitly).
227227
228228Furthermore, recursive calls under a ``Delay`` must be guarded by a constructor
229229to pass the totality checker.
@@ -387,10 +387,16 @@ Totality
387387::
388388
389389 total
390− implicit
391390 partial
392391 covering
393392
393+Implicit Coercion
394+^^^^^^^^^^^^^^^^^
395+
396+::
397+
398+ implicit
399+
394400Options
395401^^^^^^^
396402
docs/st/composing.rst+1−1
@@ -437,7 +437,7 @@ using the SDL bindings as follows:
437437
438438.. code-block:: idris
439439
440− interface Draw IO where
440+ implementation Draw IO where
441441 Surface = State SDLSurface
442442
443443 initWindow x y = do Just srf <- lift (startSDL x y)
docs/tutorial/interfaces.rst+2−2
@@ -48,8 +48,8 @@ For example, the
4848Only one implementation of an interface can be given for a type — implementations may
4949not overlap. Implementation declarations can themselves have constraints.
5050To help with resolution, the arguments of an implementation must be
51−constructors (either data or type constructors), variables or
52−constants (i.e. you cannot give an implementation for a function). For
51+constructors (either data or type constructors) or variables
52+(i.e. you cannot give an implementation for a function). For
5353example, to define a ``Show`` implementation for vectors, we need to know
5454that there is a ``Show`` implementation for the element type, because we are
5555going to use it to convert each element to a ``String``:
docs/tutorial/miscellany.rst+9
@@ -494,6 +494,15 @@ And for use in the browser:
494494 %include JavaScript "path/to/external.js"
495495
496496The given files will be added to the top of the generated code.
497+For library packages you can also use the ipkg objs option to include the
498+js file in the installation, and use
499+
500+.. code-block:: idris
501+
502+ %include Node "package/external.js"
503+
504+This javascript and node backends idris will also lookup for the file on
505+on that location.
497506
498507Including *NodeJS* modules
499508--------------------------
idris.cabal+16−38
@@ -1,5 +1,5 @@
11Name: idris
2−Version: 1.0
2+Version: 1.1.0
33License: BSD3
44License-file: LICENSE
55Author: Edwin Brady
@@ -40,11 +40,11 @@ Description: Idris is a general purpose language with full dependent types.
4040 .
4141 * Hugs style interactive environment
4242
43−Cabal-Version: >= 1.8.1
43+Cabal-Version: >= 1.18
4444
4545Build-type: Custom
4646
47−Tested-With: GHC == 7.6.3, GHC == 7.8.4, GHC == 7.10.3, GHC == 8.0.1
47+Tested-With: GHC == 7.10.3, GHC == 8.0.1
4848
4949Data-files: idrisdoc/styles.css
5050 jsrts/jsbn/jsbn-browser.js
@@ -196,6 +196,7 @@ Library
196196 , Idris.Output
197197 , Idris.Main
198198 , Idris.ModeCommon
199+ , Idris.Options
199200 , Idris.Parser
200201 , Idris.Parser.Helpers
201202 , Idris.Parser.Ops
@@ -258,7 +259,7 @@ Library
258259 , Tools_idris
259260
260261 Build-depends: base >=4 && <5
261− , aeson >= 0.6 && < 1.2
262+ , aeson >= 0.6 && < 1.3
262263 , annotated-wl-pprint >= 0.7 && < 0.8
263264 , ansi-terminal < 0.7
264265 , ansi-wl-pprint < 0.7
@@ -276,20 +277,22 @@ Library
276277 , filepath < 1.5
277278 , fingertree >= 0.1 && < 0.2
278279 , haskeline >= 0.7 && < 0.8
279− , ieee754 >= 0.7 && <= 0.8.0
280+ , ieee754 >= 0.7 && < 0.9
280281 , mtl >= 2.1 && < 2.3
281282 , network < 2.7
282− , optparse-applicative >= 0.11 && < 0.14
283+ , optparse-applicative >= 0.13 && < 0.15
283284 , parsers >= 0.9 && < 0.13
284285 , pretty < 1.2
286+ , process < 1.7
285287 , regex-tdfa >= 1.2
288+ , safe >= 0.3.9
286289 , split < 0.3
287290 , terminal-size < 0.4
288291 , text >=1.2.1.0 && < 1.3
289− , time >= 1.4 && < 1.7
292+ , time >= 1.4 && < 1.9
290293 , transformers < 0.6
291294 , transformers-compat >= 0.3
292− , trifecta >= 1.6 && < 1.7
295+ , trifecta >= 1.6 && < 1.8
293296 , uniplate >=1.6 && < 1.7
294297 , unordered-containers < 0.3
295298 , utf8-string < 1.1
@@ -299,34 +302,6 @@ Library
299302 , fsnotify >= 0.2 && < 2.2
300303 , async < 2.2
301304
302−
303− -- zlib >= 0.6.1 is broken with GHC < 7.10.3
304− -- Travis is broken for 7.6 and 7.8 with a newer process
305− if impl(ghc < 7.10.3)
306− build-depends: zlib < 0.6.1
307− , process < 1.3
308− else
309− build-depends: process < 1.5
310−
311− -- safe 0.3.10 is having issues with cabal 1.20 and ghc 7.6.3, the
312− -- hvr ghc ppa doesn't provide a new enough cabal library. Temporary
313− -- fix until hvr ghc ppa is fixed or we deprecate support for 7.6.3.
314− if impl(ghc < 7.8.4)
315− build-depends: safe == 0.3.9
316− else
317− build-depends: safe >= 0.3.9
318−
319− if impl(ghc < 7.8.4)
320− build-depends: tagsoup < 0.14.1
321−
322− Extensions: MultiParamTypeClasses
323− , DeriveFoldable
324− , DeriveTraversable
325− , FunctionalDependencies
326− , FlexibleContexts
327− , FlexibleInstances
328− , TemplateHaskell
329−
330305 ghc-prof-options: -auto-all -caf-all
331306
332307 if os(linux)
@@ -364,6 +339,7 @@ Executable idris
364339 , haskeline >= 0.7
365340 , transformers
366341
342+ Default-Language: Haskell2010
367343 ghc-prof-options: -auto-all -caf-all
368344 ghc-options: -threaded -rtsopts -funbox-strict-fields -with-rtsopts=-I0
369345
@@ -388,10 +364,9 @@ Test-suite regression-and-feature-tests
388364 , tasty-rerun >= 1.0.0
389365 , bytestring
390366 , transformers
391− if impl(ghc < 7.10)
392− Extensions: DeriveDataTypeable
393367
394368
369+ Default-Language: Haskell2010
395370 ghc-prof-options: -auto-all -caf-all
396371 ghc-options: -threaded -rtsopts -with-rtsopts=-N -funbox-strict-fields
397372
@@ -405,6 +380,7 @@ Executable idris-codegen-c
405380 , haskeline >= 0.7
406381 , transformers
407382
383+ Default-Language: Haskell2010
408384 ghc-prof-options: -auto-all -caf-all
409385 ghc-options: -threaded -rtsopts -funbox-strict-fields
410386
@@ -418,6 +394,7 @@ Executable idris-codegen-javascript
418394 , haskeline >= 0.7
419395 , transformers
420396
397+ Default-Language: Haskell2010
421398 ghc-prof-options: -auto-all -caf-all
422399 ghc-options: -threaded -rtsopts -funbox-strict-fields
423400
@@ -431,5 +408,6 @@ Executable idris-codegen-node
431408 , haskeline >= 0.7
432409 , transformers
433410
411+ Default-Language: Haskell2010
434412 ghc-prof-options: -auto-all -caf-all
435413 ghc-options: -threaded -rtsopts -funbox-strict-fields
libs/base/Control/Catchable.idr+22
@@ -1,6 +1,10 @@
11module Control.Catchable
22
33import Control.IOExcept
4+import Control.Monad.Reader
5+import Control.Monad.Writer
6+import Control.Monad.RWS
7+import Control.Monad.Trans
48
59%access public export
610
@@ -32,3 +36,21 @@ implementation Catchable List () where
3236 catch xs h = xs
3337
3438 throw () = []
39+
40+||| Adapted from https://hackage.haskell.org/package/mtl-2.2.1/docs/src/Control.Monad.Error.Class.html#line-138
41+implementation (Monad m, Catchable m t) => Catchable (ReaderT r m) t where
42+ -- TODO: rewrite this with apply2way combinator when implemented
43+ catch m h = RD $ \ r => catch (runReaderT m r) (\ e => runReaderT (h e) r)
44+ -- catch m h = RD $ \ r => catch (runReaderT m r) (\ e => runReaderT (h e) r)
45+
46+ throw = lift . throw
47+
48+||| Adapted from https://hackage.haskell.org/package/transformers-0.5.4.0/docs/src/Control.Monad.Trans.Writer.Lazy.html#local-6989586621679059673
49+implementation (Monad m, Monoid w, Catchable m t) => Catchable (WriterT w m) t where
50+ catch m h = WR $ runWriterT m `catch` runWriterT . h
51+ throw = lift . throw
52+
53+||| Adapted from https://hackage.haskell.org/package/mtl-2.2.1/docs/src/Control.Monad.Error.Class.html#line-138
54+implementation (Monad m, Monoid w, Catchable m t) => Catchable (RWST r w s m) t where
55+ catch m h = MkRWST $ \ r, s => runRWST m r s `catch` \ e => runRWST (h e) r s
56+ throw = lift . throw
libs/base/Control/Monad/RWS.idr+7−1
@@ -14,7 +14,7 @@ interface (Monoid w, MonadReader r m, MonadWriter w m, MonadState s m) => MonadR
1414record RWST (r : Type) (w : Type) (s : Type) (m : Type -> Type) (a : Type) where
1515 constructor MkRWST
1616 runRWST : r -> s -> m (a, s, w)
17−
17+
1818implementation Monad m => Functor (RWST r w s m) where
1919 map f (MkRWST m) = MkRWST $ \r,s => do (a, s', w) <- m r s
2020 pure (f a, s', w)
@@ -48,6 +48,12 @@ implementation (Monoid w, Monad m) => MonadState s (RWST r w s m) where
4848
4949implementation (Monoid w, Monad m) => MonadRWS r w s (RWST r w s m) where {}
5050
51+||| Adapted from https://hackage.haskell.org/package/transformers-0.5.4.0/docs/src/Control-Monad-Trans-RWS-Lazy.html
52+implementation Monoid w => MonadTrans (RWST r w s) where
53+ lift x = MkRWST $ \ _, s => do
54+ a <- x
55+ pure (a, s, neutral)
56+
5157||| The RWS monad. See the MonadRWS interface
5258RWS : Type -> Type -> Type -> Type -> Type
5359RWS r w s a = RWST r w s Identity a
libs/base/Data/List/Views.idr+17−21
@@ -61,22 +61,18 @@ data SplitRec : List a -> Type where
6161 (lrec : Lazy (SplitRec lefts)) ->
6262 (rrec : Lazy (SplitRec rights)) -> SplitRec (lefts ++ rights)
6363
64−total
65−splitRecFix : (xs : List a) -> ((ys : List a) -> smaller ys xs -> SplitRec ys) ->
66− SplitRec xs
67−splitRecFix xs srec with (split xs)
68− splitRecFix [] srec | SplitNil = SplitRecNil
69− splitRecFix [x] srec | SplitOne = SplitRecOne
70− splitRecFix (x :: (ys ++ (y :: zs))) srec | SplitPair
71− = let left = srec (x :: ys) (smallerLeft ys y zs)
72− right = srec (y :: zs) (smallerRight ys zs) in
73− SplitRecPair left right
74−
7564||| Covering function for the `SplitRec` view
7665||| Constructs the view in O(n lg n)
77−export total
66+public export total
7867splitRec : (xs : List a) -> SplitRec xs
79−splitRec xs = accInd splitRecFix xs (smallerAcc xs)
68+splitRec xs with (sizeAccessible xs)
69+ splitRec xs | acc with (split xs)
70+ splitRec [] | acc | SplitNil = SplitRecNil
71+ splitRec [x] | acc | SplitOne = SplitRecOne
72+ splitRec (y :: ys ++ z :: zs) | Access acc | SplitPair
73+ = SplitRecPair
74+ (splitRec (y :: ys) | acc _ (smallerLeft ys z zs))
75+ (splitRec (z :: zs) | acc _ (smallerRight ys zs))
8076
8177||| View for traversing a list backwards
8278public export
@@ -105,21 +101,21 @@ data Filtered : (a -> a -> Bool) -> List a -> Type where
105101 (rrec : Lazy (Filtered p (filter (\y => not (p y x)) xs))) ->
106102 Filtered p (x :: xs)
107103
108−filteredLOK : (p : a -> a -> Bool) -> (x : a) -> (xs : List a) -> smaller (filter (\y => p y x) xs) (x :: xs)
104+filteredLOK : (p : a -> a -> Bool) -> (x : a) -> (xs : List a) -> Smaller (filter (\y => p y x) xs) (x :: xs)
109105filteredLOK p x xs = LTESucc (filterSmaller xs)
110106
111−filteredROK : (p : a -> a -> Bool) -> (x : a) -> (xs : List a) -> smaller (filter (\y => not (p y x)) xs) (x :: xs)
107+filteredROK : (p : a -> a -> Bool) -> (x : a) -> (xs : List a) -> Smaller (filter (\y => not (p y x)) xs) (x :: xs)
112108filteredROK p x xs = LTESucc (filterSmaller xs)
113109
114110||| Covering function for the `Filtered` view
115111||| Constructs the view in O(n lg n)
116−export
112+public export total
117113filtered : (p : a -> a -> Bool) -> (xs : List a) -> Filtered p xs
118−filtered p inp with (smallerAcc inp)
119− filtered p [] | with_pat = FNil
120− filtered p (x :: xs) | (Access xsrec)
121− = FRec (filtered p (filter (\y => p y x) xs) | xsrec _ (filteredLOK p x xs))
122− (filtered p (filter (\y => not (p y x)) xs) | xsrec _ (filteredROK p x xs))
114+filtered p inp with (sizeAccessible inp)
115+ filtered p [] | _ = FNil
116+ filtered p (x :: xs) | Access acc
117+ = FRec (filtered p (filter (\y => p y x) xs) | acc _ (filteredLOK p x xs))
118+ (filtered p (filter (\y => not (p y x)) xs) | acc _ (filteredROK p x xs))
123119
124120lenImpossible : (n = Z) -> (n = ((S k) + right)) -> Void
125121lenImpossible {n = Z} _ Refl impossible
libs/base/Data/Nat/Views.idr+9−13
@@ -22,17 +22,13 @@ half (S k) with (half k)
2222 HalfEven {n=S n}
2323 half (S (n + n)) | HalfEven = HalfOdd
2424
25−halfRecFix : (n : Nat) -> ((m : Nat) -> LT m n -> HalfRec m) -> HalfRec n
26−halfRecFix Z hrec = HalfRecZ
27−halfRecFix (S k) hrec with (half k)
28− halfRecFix (S (S (n + n))) hrec | HalfOdd
29− = rewrite plusSuccRightSucc (S n) n in
30− HalfRecEven (hrec (S n) (LTESucc (LTESucc (lteAddRight _))))
31− halfRecFix (S (n + n)) hrec | HalfEven
32− = HalfRecOdd (hrec n (LTESucc (lteAddRight _)))
33−
34−||| Covering function for the `HalfRec` view
35−export
25+public export total
3626halfRec : (n : Nat) -> HalfRec n
37−halfRec n = accInd halfRecFix n (ltAccessible n)
38−
27+halfRec n with (sizeAccessible n)
28+ halfRec Z | acc = HalfRecZ
29+ halfRec (S n) | acc with (half n)
30+ halfRec' (S (S (k + k))) | Access acc | HalfOdd
31+ = rewrite plusSuccRightSucc (S k) k
32+ in HalfRecEven (halfRec' (S k) | acc (S k) (LTESucc (LTESucc (lteAddRight _))))
33+ halfRec' (S (k + k)) | Access acc | HalfEven
34+ = HalfRecOdd (halfRec' k | acc k (LTESucc (lteAddRight _)))
libs/base/Data/Vect/Views.idr+10−10
@@ -61,23 +61,23 @@ data SplitRec : Vect n a -> Type where
6161 (lrec : Lazy (SplitRec xs)) ->
6262 (rrec : Lazy (SplitRec ys)) -> SplitRec (xs ++ ys)
6363
64−smallerPlus : LTE (S (S m)) (S (plus m (S k)))
65−smallerPlus {m} {k} = rewrite sym (plusSuccRightSucc m k) in
64+smallerPlusL : LTE (S (S m)) (S (plus m (S k)))
65+smallerPlusL {m} {k} = rewrite sym (plusSuccRightSucc m k) in
6666 (LTESucc (LTESucc (lteAddRight _)))
6767
68−smallerPlus' : LTE (S (S k)) (S (plus m (S k)))
69−smallerPlus' {m} {k} = rewrite sym (plusSuccRightSucc m k) in
68+smallerPlusR : LTE (S (S k)) (S (plus m (S k)))
69+smallerPlusR {m} {k} = rewrite sym (plusSuccRightSucc m k) in
7070 LTESucc (LTESucc (rewrite plusCommutative m k in (lteAddRight _)))
7171
7272||| Covering function for the `SplitRec` view
7373||| Constructs the view in O(n lg n)
74−export
74+public export total
7575splitRec : (xs : Vect n a) -> SplitRec xs
76−splitRec {n} input with (ltAccessible n)
76+splitRec {n} input with (sizeAccessible n)
7777 splitRec input | acc with (split input)
7878 splitRec [] | acc | SplitNil = SplitRecNil
7979 splitRec [x] | acc | SplitOne = SplitRecOne
80− splitRec (x :: (xs ++ (y :: ys))) | (Access rec) | SplitPair
81− = let left = splitRec (x :: xs) | rec _ smallerPlus
82− right = splitRec (y :: ys) | rec _ smallerPlus' in
83− SplitRecPair left right
80+ splitRec (x :: (xs ++ (y :: ys))) | Access acc | SplitPair
81+ = SplitRecPair
82+ (splitRec (x :: xs) | acc _ smallerPlusL)
83+ (splitRec (y :: ys) | acc _ smallerPlusR)
libs/contrib/Data/Heap.idr−4
@@ -132,10 +132,6 @@ implementation Ord a => Monoid (MaxiphobicHeap a) where
132132-- Properties
133133--------------------------------------------------------------------------------
134134
135−total
136−absurdBoolDischarge : False = True -> Void
137−absurdBoolDischarge Refl impossible
138−
139135total
140136isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = Z
141137isEmptySizeZero Empty p = Refl
libs/contrib/Data/SortedMap.idr+52−1
@@ -1,6 +1,6 @@
11module Data.SortedMap
22
3−-- TODO: write merge and split
3+-- TODO: write split
44
55private
66data Tree : Nat -> (k : Type) -> Type -> Ord k -> Type where
@@ -214,6 +214,10 @@ insert k v (M _ t) =
214214 Left t' => (M _ t')
215215 Right t' => (M _ t')
216216
217+export
218+insertFrom : Foldable f => f (k, v) -> SortedMap k v -> SortedMap k v
219+insertFrom = flip $ foldl $ flip $ uncurry insert
220+
217221export
218222delete : k -> SortedMap k v -> SortedMap k v
219223delete _ Empty = Empty
@@ -235,6 +239,16 @@ toList : SortedMap k v -> List (k, v)
235239toList Empty = []
236240toList (M _ t) = treeToList t
237241
242+||| Gets the keys of the map.
243+export
244+keys : SortedMap k v -> List k
245+keys = map fst . toList
246+
247+||| Gets the values of the map. Could contain duplicates.
248+export
249+values : SortedMap k v -> List v
250+values = map snd . toList
251+
238252treeMap : (a -> b) -> Tree n k a o -> Tree n k b o
239253treeMap f (Leaf k v) = Leaf k (f v)
240254treeMap f (Branch2 t1 k t2) = Branch2 (treeMap f t1) k (treeMap f t2)
@@ -245,3 +259,40 @@ export
245259implementation Functor (SortedMap k) where
246260 map _ Empty = Empty
247261 map f (M n t) = M _ (treeMap f t)
262+
263+||| Merge two maps. When encountering duplicate keys, using a function to combine the values.
264+||| Uses the ordering of the first map given.
265+export
266+mergeWith : (v -> v -> v) -> SortedMap k v -> SortedMap k v -> SortedMap k v
267+mergeWith f x y = insertFrom inserted x where
268+ inserted : List (k, v)
269+ inserted = do
270+ (k, v) <- toList y
271+ let v' = (maybe id f $ lookup k x) v
272+ pure (k, v')
273+
274+||| Merge two maps using the Semigroup (and by extension, Monoid) operation.
275+||| Uses mergeWith internally, so the ordering of the left map is kept.
276+export
277+merge : Semigroup v => SortedMap k v -> SortedMap k v -> SortedMap k v
278+merge = mergeWith (<+>)
279+
280+||| Left-biased merge, also keeps the ordering specified by the left map.
281+export
282+mergeLeft : SortedMap k v -> SortedMap k v -> SortedMap k v
283+mergeLeft = mergeWith const
284+
285+-- TODO: is this the right variant of merge to use for this? I think it is, but
286+-- I could also see the advantages of using `mergeLeft`. The current approach is
287+-- strictly more powerful I believe, because `mergeLeft` can be emulated with
288+-- the `First` monoid. However, this does require more code to do the same
289+-- thing.
290+export
291+Semigroup v => Semigroup (SortedMap k v) where
292+ (<+>) = merge
293+
294+||| For `neutral <+> y`, y is rebuilt in `Ord k`, so this is not a "strict" Monoid.
295+||| However, semantically, it should be equal.
296+export
297+(Ord k, Semigroup v) => Monoid (SortedMap k v) where
298+ neutral = empty
libs/contrib/Data/SortedSet.idr+4
@@ -60,3 +60,7 @@ Ord k => Semigroup (SortedSet k) where
6060export
6161Ord k => Monoid (SortedSet k) where
6262 neutral = empty
63+
64+export
65+keySet : SortedMap k v -> SortedSet k
66+keySet = SetWrapper . map (const ())
libs/contrib/Text/Lexer.idrnew file+238
@@ -0,0 +1,238 @@
1+module Text.Lexer
2+
3+%default total
4+
5+||| A language of token recognisers.
6+||| The `consumes` flag is True is the recogniser is guaranteed to consume
7+||| at least one character
8+export
9+data Recognise : (consumes : Bool) -> Type where
10+ Empty : Recognise False
11+ Fail : Recognise c
12+ Pred : (Char -> Bool) -> Recognise True
13+ SeqEat : Recognise True -> Inf (Recognise e) -> Recognise True
14+ SeqEmpty : Recognise e1 -> Recognise e2 -> Recognise (e1 || e2)
15+ Alt : Recognise e1 -> Recognise e2 -> Recognise (e1 && e2)
16+
17+||| A token recogniser. Guaranteed to consume at least one character.
18+public export
19+Lexer : Type
20+Lexer = Recognise True
21+
22+public export
23+inf : Bool -> Type -> Type
24+inf True t = Inf t
25+inf False t = t
26+
27+||| Sequence two recognisers. If either consumes a character, the sequence
28+||| is guaranteed to consume a character.
29+export %inline
30+(<+>) : {c1 : Bool} ->
31+ Recognise c1 -> inf c1 (Recognise c2) -> Recognise (c1 || c2)
32+(<+>) {c1 = False} = SeqEmpty
33+(<+>) {c1 = True} = SeqEat
34+
35+||| Alternative recognisers. If both consume, the combination is guaranteed
36+||| to consumer a character.
37+export
38+(<|>) : Recognise c1 -> Recognise c2 -> Recognise (c1 && c2)
39+(<|>) = Alt
40+
41+||| Recognise a specific character
42+export
43+is : Char -> Lexer
44+is x = Pred (==x)
45+
46+||| Recognise anything but the given character
47+export
48+isNot : Char -> Lexer
49+isNot x = Pred (/=x)
50+
51+||| Recognise a sequence of at least one sub-lexers
52+export
53+some : Lexer -> Lexer
54+some l = l <+> (some l <|> Empty)
55+
56+||| Recognise a sequence of at zero or more sub-lexers. This is not
57+||| guaranteed to consume input
58+export
59+many : Lexer -> Recognise False
60+many l = some l <|> Empty
61+
62+||| Recognise any character
63+export
64+any : Lexer
65+any = Pred (const True)
66+
67+||| Recognise no input (doesn't consume any input)
68+export
69+empty : Recognise False
70+empty = Empty
71+
72+||| Recognise a character that matches a predicate
73+export
74+pred : (Char -> Bool) -> Lexer
75+pred = Pred
76+
77+||| Recognise any of the characters in the given string
78+export
79+oneOf : String -> Lexer
80+oneOf cs = pred (\x => x `elem` unpack cs)
81+
82+data StrLen : Type where
83+ MkStrLen : String -> Nat -> StrLen
84+
85+getString : StrLen -> String
86+getString (MkStrLen str n) = str
87+
88+strIndex : StrLen -> Nat -> Maybe Char
89+strIndex (MkStrLen str len) i
90+ = if i >= len then Nothing
91+ else Just (assert_total (prim__strIndex str (cast i)))
92+
93+mkStr : String -> StrLen
94+mkStr str = MkStrLen str (length str)
95+
96+strTail : Nat -> StrLen -> StrLen
97+strTail start (MkStrLen str len)
98+ = MkStrLen (substr start len str) (minus len start)
99+
100+-- If the string is recognised, returns the index at which the token
101+-- ends
102+scan : Recognise c -> Nat -> StrLen -> Maybe Nat
103+scan Empty idx str = pure idx
104+scan Fail idx str = Nothing
105+scan (Pred f) idx str
106+ = do c <- strIndex str idx
107+ if f c
108+ then Just (idx + 1)
109+ else Nothing
110+scan (SeqEat r1 r2) idx str
111+ = do idx' <- scan r1 idx str
112+ -- TODO: Can we prove totality instead by showing idx has increased?
113+ assert_total (scan r2 idx' str)
114+scan (SeqEmpty r1 r2) idx str
115+ = do idx' <- scan r1 idx str
116+ scan r2 idx' str
117+scan (Alt r1 r2) idx str
118+ = case scan r1 idx str of
119+ Nothing => scan r2 idx str
120+ Just idx => Just idx
121+
122+takeToken : Lexer -> StrLen -> Maybe (String, StrLen)
123+takeToken lex str
124+ = do i <- scan lex 0 str -- i must be > 0 if successful
125+ pure (substr 0 i (getString str), strTail i str)
126+
127+||| Recognise a digit 0-9
128+export
129+digits : Lexer
130+digits = some (Pred isDigit)
131+
132+||| Recognise a specific string
133+export
134+exact : String -> Lexer
135+exact str with (unpack str)
136+ exact str | [] = Fail -- Not allowed, Lexer has to consume
137+ exact str | (x :: xs)
138+ = foldl SeqEmpty (is x) (map is xs)
139+
140+||| Recognise a whitespace character
141+export
142+space : Lexer
143+space = some (pred isSpace)
144+
145+||| Recognise a non-alphanumeric, non-whitespace character
146+export
147+symbol : Lexer
148+symbol = some (pred (\x => not (isAlphaNum x) && not (isSpace x)))
149+
150+strChar : Lexer
151+strChar = (is '\\' <+> any) <|> isNot '"'
152+
153+||| Recognise a string literal, including escaped characters.
154+||| (Note: doesn't yet handle escape sequences such as \123)
155+export
156+stringLit : Lexer
157+stringLit = is '"' <+> many strChar <+> is '"'
158+
159+||| Recognise a character literal, including escaped characters.
160+||| (Note: doesn't yet handle escape sequences such as \123)
161+export
162+charLit : Lexer
163+charLit = is '\'' <+> strChar <+> is '\''
164+
165+||| Recognise an integer literal (possibly with a '-' prefix)
166+export
167+intLit : Lexer
168+intLit = (is '-' <|> Empty) <+> digits
169+
170+||| A mapping from lexers to the tokens they produce.
171+||| This is a list of pairs `(Lexer, String -> tokenType)`
172+||| For each Lexer in the list, if a substring in the input matches, run
173+||| the associated function to produce a token of type `tokenType`
174+public export
175+TokenMap : (tokenType : Type) -> Type
176+TokenMap tokenType = List (Lexer, String -> tokenType)
177+
178+||| A token, and the line and column where it was in the input
179+public export
180+record TokenData a where
181+ constructor MkToken
182+ line : Int
183+ col : Int
184+ tok : a
185+
186+fspanEnd : Nat -> (Char -> Bool) -> String -> (Nat, String)
187+fspanEnd k p "" = (k, "")
188+fspanEnd k p xxs
189+ = assert_total $
190+ let x = prim__strHead xxs
191+ xs = prim__strTail xxs in
192+ if p x then fspanEnd (S k) p xs
193+ else (k, xxs)
194+
195+-- Faster version of 'span' from the prelude (avoids unpacking)
196+export
197+fspan : (Char -> Bool) -> String -> (String, String)
198+fspan p xs
199+ = let (end, rest) = fspanEnd 0 p xs in
200+ (substr 0 end xs, rest)
201+
202+tokenise : (line : Int) -> (col : Int) ->
203+ List (TokenData a) -> TokenMap a ->
204+ StrLen -> (List (TokenData a), (Int, Int, StrLen))
205+tokenise line col acc tmap str
206+ = case getFirstToken tmap str of
207+ Just (tok, line', col', rest) =>
208+ -- assert total because getFirstToken must consume something
209+ assert_total (tokenise line' col' (tok :: acc) tmap rest)
210+ Nothing => (reverse acc, (line, col, str))
211+ where
212+ countNLs : List Char -> Nat
213+ countNLs str = List.length (filter (== '\n') str)
214+
215+ getCols : String -> Int -> Int
216+ getCols x c
217+ = case fspan (/= '\n') (reverse x) of
218+ (incol, "") => c + cast (length incol)
219+ (incol, _) => cast (length incol)
220+
221+ getFirstToken : TokenMap a -> StrLen -> Maybe (TokenData a, Int, Int, StrLen)
222+ getFirstToken [] str = Nothing
223+ getFirstToken ((lex, fn) :: ts) str
224+ = case takeToken lex str of
225+ Just (tok, rest) => Just (MkToken line col (fn tok),
226+ line + cast (countNLs (unpack tok)),
227+ getCols tok col, rest)
228+ Nothing => getFirstToken ts str
229+
230+||| Given a mapping from lexers to token generating functions (the
231+||| TokenMap a) and an input string, return a list of recognised tokens,
232+||| and the line, column, and remainder of the input at the first point in the
233+||| string where there are no recognised tokens.
234+export
235+lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))
236+lex tmap str = let (ts, (l, c, str')) = tokenise 0 0 [] tmap (mkStr str) in
237+ (ts, (l, c, getString str'))
238+
libs/contrib/Text/Parser.idrnew file+229
@@ -0,0 +1,229 @@
1+module Text.Parser
2+
3+%default total
4+
5+-- TODO: Add some primitives for helping with error messages.
6+-- e.g. perhaps set a string to state what we're currently trying to
7+-- parse, or to say what the next expected token is in words
8+
9+||| Description of a language's grammar. The `tok` parameter is the type
10+||| of tokens, and the `consumes` flag is True if the language is guaranteed
11+||| to be non-empty - that is, successfully parsing the language is guaranteed
12+||| to consume some input.
13+export
14+data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where
15+ Empty : (val : ty) -> Grammar tok False ty
16+ Terminal : (tok -> Maybe a) -> Grammar tok True a
17+ NextIs : (tok -> Bool) -> Grammar tok False tok
18+ EOF : Grammar tok False ()
19+
20+ Fail : String -> Grammar tok c ty
21+ Commit : Grammar tok False ()
22+
23+ SeqEat : Grammar tok True a -> Inf (a -> Grammar tok c2 b) ->
24+ Grammar tok True b
25+ SeqEmpty : {c1, c2 : Bool} ->
26+ Grammar tok c1 a -> (a -> Grammar tok c2 b) ->
27+ Grammar tok (c1 || c2) b
28+ Alt : {c1, c2 : Bool} ->
29+ Grammar tok c1 ty -> Grammar tok c2 ty ->
30+ Grammar tok (c1 && c2) ty
31+
32+public export
33+inf : Bool -> Type -> Type
34+inf True t = Inf t
35+inf False t = t
36+
37+||| Sequence two grammars. If either consumes some input, the sequence is
38+||| guaranteed to consume some input. If the first one consumes input, the
39+||| second is allowed to be recursive (because it means some input has been
40+||| consumed and therefore the input is smaller)
41+export %inline
42+(>>=) : {c1 : Bool} ->
43+ Grammar tok c1 a -> inf c1 (a -> Grammar tok c2 b) ->
44+ Grammar tok (c1 || c2) b
45+(>>=) {c1 = False} = SeqEmpty
46+(>>=) {c1 = True} = SeqEat
47+
48+||| Give two alternative grammars. If both consume, the combination is
49+||| guaranteed to consume.
50+export
51+(<|>) : Grammar tok c1 ty -> Grammar tok c2 ty ->
52+ Grammar tok (c1 && c2) ty
53+(<|>) = Alt
54+
55+export
56+pure : (val : ty) -> Grammar tok False ty
57+pure = Empty
58+
59+||| Check whether the next token satisfies a predicate
60+export
61+nextIs : (tok -> Bool) -> Grammar tok False tok
62+nextIs = NextIs
63+
64+||| Look at the next token in the input
65+export
66+peek : Grammar tok False tok
67+peek = nextIs (const True)
68+
69+||| Succeeds if running the predicate on the next token returns Just x,
70+||| returning x. Otherwise fails.
71+export
72+terminal : (tok -> Maybe a) -> Grammar tok True a
73+terminal = Terminal
74+
75+||| Always fail with a message
76+export
77+fail : String -> Grammar tok c ty
78+fail = Fail
79+
80+||| Succeed if the input is empty
81+export
82+eof : Grammar tok False ()
83+eof = EOF
84+
85+||| Commit to an alternative; if the current branch of an alternative
86+||| fails to parse, no more branches will be tried
87+export
88+commit : Grammar tok False ()
89+commit = Commit
90+
91+data ParseResult : List tok -> (consumes : Bool) -> Type -> Type where
92+ Failure : {xs : List tok} ->
93+ (committed : Bool) ->
94+ (err : String) -> (rest : List tok) -> ParseResult xs c ty
95+ EmptyRes : (committed : Bool) ->
96+ (val : ty) -> (more : List tok) -> ParseResult more False ty
97+ NonEmptyRes : (committed : Bool) ->
98+ (val : ty) -> (more : List tok) ->
99+ ParseResult (x :: xs ++ more) c ty
100+
101+weakenRes : {whatever, c : Bool} -> {xs : List tok} ->
102+ ParseResult xs c ty -> ParseResult xs (whatever && c) ty
103+weakenRes (Failure com msg ts) = Failure com msg ts
104+weakenRes {whatever=True} (EmptyRes com val xs) = EmptyRes com val xs
105+weakenRes {whatever=False} (EmptyRes com val xs) = EmptyRes com val xs
106+weakenRes (NonEmptyRes com val more) = NonEmptyRes com val more
107+
108+shorter : (more : List tok) -> .(ys : List tok) ->
109+ LTE (S (length more)) (S (length (ys ++ more)))
110+shorter more [] = lteRefl
111+shorter more (x :: xs) = LTESucc (lteSuccLeft (shorter more xs))
112+
113+doParse : {c : Bool} ->
114+ (commit : Bool) -> (xs : List tok) -> (act : Grammar tok c ty) ->
115+ ParseResult xs c ty
116+doParse com xs act with (sizeAccessible xs)
117+ doParse com xs (Empty val) | sml = EmptyRes com val xs
118+ doParse com [] (Fail str) | sml = Failure com str []
119+ doParse com (x :: xs) (Fail str) | sml = Failure com str (x :: xs)
120+ doParse com xs Commit | sml = EmptyRes True () xs
121+
122+ doParse com [] (Terminal f) | sml = Failure com "End of input" []
123+ doParse com (x :: xs) (Terminal f) | sml
124+ = maybe
125+ (Failure com "Unrecognised token" (x :: xs))
126+ (\a => NonEmptyRes com {xs=[]} a xs)
127+ (f x)
128+ doParse com [] EOF | sml = EmptyRes com () []
129+ doParse com (x :: xs) EOF | sml
130+ = Failure com "Expected end of input" (x :: xs)
131+ doParse com [] (NextIs f) | sml = Failure com "End of input" []
132+ doParse com (x :: xs) (NextIs f) | sml
133+ = if f x
134+ then EmptyRes com x (x :: xs)
135+ else Failure com "Unrecognised token" (x :: xs)
136+ doParse com xs (Alt x y) | sml with (doParse False xs x | sml)
137+ doParse com xs (Alt x y) | sml | Failure com' msg ts
138+ = if com' -- If the alternative had committed, don't try the
139+ -- other branch (and reset commit flag)
140+ then Failure com msg ts
141+ else weakenRes (doParse False xs y | sml)
142+ -- Successfully parsed the first option, so use the outer commit flag
143+ doParse com xs (Alt x y) | sml | (EmptyRes _ val xs)
144+ = EmptyRes com val xs
145+ doParse com (z :: (ys ++ more)) (Alt x y) | sml | (NonEmptyRes _ val more)
146+ = NonEmptyRes com val more
147+ doParse com xs (SeqEmpty act next) | (Access morerec)
148+ = case doParse com xs act | Access morerec of
149+ Failure com msg ts => Failure com msg ts
150+ EmptyRes com val xs =>
151+ case doParse com xs (next val) | (Access morerec) of
152+ Failure com' msg ts => Failure com' msg ts
153+ EmptyRes com' val xs => EmptyRes com' val xs
154+ NonEmptyRes com' val more => NonEmptyRes com' val more
155+ NonEmptyRes {x} {xs=ys} com val more =>
156+ case (doParse com more (next val) | morerec _ (shorter more ys)) of
157+ Failure com' msg ts => Failure com' msg ts
158+ EmptyRes com' val _ => NonEmptyRes com' val more
159+ NonEmptyRes {x=x1} {xs=xs1} com' val more' =>
160+ rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in
161+ NonEmptyRes com' val more'
162+ doParse com xs (SeqEat act next) | sml with (doParse com xs act | sml)
163+ doParse com xs (SeqEat act next) | sml | Failure com' msg ts
164+ = Failure com' msg ts
165+ doParse com (x :: (ys ++ more)) (SeqEat act next) | (Access morerec) | (NonEmptyRes com' val more)
166+ = case doParse com' more (next val) | morerec _ (shorter more ys) of
167+ Failure com' msg ts => Failure com' msg ts
168+ EmptyRes com' val _ => NonEmptyRes com' val more
169+ NonEmptyRes {x=x1} {xs=xs1} com' val more' =>
170+ rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in
171+ NonEmptyRes com' val more'
172+ -- This next line is not strictly necessary, but it stops the coverage
173+ -- checker taking a really long time and eating lots of memory...
174+ doParse _ _ _ | sml = Failure True "Help the coverage checker!" []
175+
176+public export
177+data ParseError tok = Error String (List tok)
178+
179+||| Parse a list of tokens according to the given grammar. If successful,
180+||| returns a pair of the parse result and the unparsed tokens (the remaining
181+||| input).
182+export
183+parse : (xs : List tok) -> (act : Grammar tok c ty) ->
184+ Either (ParseError tok) (ty, List tok)
185+parse xs act
186+ = case doParse False xs act of
187+ Failure _ msg ts => Left (Error msg ts)
188+ EmptyRes _ val rest => pure (val, rest)
189+ NonEmptyRes _ val rest => pure (val, rest)
190+
191+||| Parse one or more things
192+export
193+some : Grammar tok True a ->
194+ Grammar tok True (List a)
195+some p = do x <- p
196+ (do xs <- some p
197+ pure (x :: xs)) <|> pure [x]
198+
199+||| Parse zero or more things (may match the empty input)
200+export
201+many : Grammar tok True a ->
202+ Grammar tok False (List a)
203+many p = some p
204+ <|> pure []
205+
206+||| Parse one or more things, separated by another thing
207+export
208+sepBy1 : Grammar tok True () -> Grammar tok True a ->
209+ Grammar tok True (List a)
210+sepBy1 sep p = do x <- p
211+ (do sep
212+ xs <- sepBy1 sep p
213+ pure (x :: xs)) <|> pure [x]
214+
215+||| Parse zero or more things, separated by another thing. May
216+||| match the empty input.
217+export
218+sepBy : Grammar tok True () -> Grammar tok True a ->
219+ Grammar tok False (List a)
220+sepBy sep p = sepBy1 sep p <|> pure []
221+
222+||| Optionally parse a thing, with a default value if the grammar doesn't
223+||| match. May match the empty input.
224+export
225+optional : Grammar tok True a -> (ifNothing : a) ->
226+ Grammar tok False a
227+optional p def = p <|> pure def
228+
229+
libs/contrib/Text/PrettyPrint/WL.idrnew file+18
@@ -0,0 +1,18 @@
1+||| A revised Idris port of the Wadler-Leijen pretty-printer.
2+|||
3+||| This port of the Wadler-Leijen Pretty-Printer is based upon the
4+||| port originally created by Shayan Najd [1]. We have changed the
5+||| render function to be total using a technique based on
6+||| continuations proposed by gallais [2], and fix minor errors in the
7+||| original Idris port.
8+|||
9+||| [1] https://github.com/shayan-najd/wl-pprint
10+||| [2] https://gallais.github.io/blog/termination-tricks.html
11+module Text.PrettyPrint.WL
12+
13+import public Text.PrettyPrint.WL.Core
14+import public Text.PrettyPrint.WL.Characters
15+import public Text.PrettyPrint.WL.Combinators
16+
17+%default total
18+%access export
libs/contrib/Text/PrettyPrint/WL/Characters.idrnew file+103
@@ -0,0 +1,103 @@
1+||| Commonly used characters
2+module Text.PrettyPrint.WL.Characters
3+
4+import Text.PrettyPrint.WL.Core
5+
6+%default total
7+%access export
8+
9+lparen : Doc
10+lparen = char '('
11+
12+rparen : Doc
13+rparen = char ')'
14+
15+langle : Doc
16+langle = char '<'
17+
18+rangle : Doc
19+rangle = char '>'
20+
21+lbrace : Doc
22+lbrace = char '{'
23+
24+rbrace : Doc
25+rbrace = char '}'
26+
27+lbracket : Doc
28+lbracket = char '['
29+
30+rbracket : Doc
31+rbracket = char ']'
32+
33+squote : Doc
34+squote = char '\''
35+
36+dquote : Doc
37+dquote = char '"'
38+
39+semi : Doc
40+semi = char ';'
41+
42+colon : Doc
43+colon = char ':'
44+
45+comma : Doc
46+comma = char ','
47+
48+space : Doc
49+space = char ' '
50+
51+dot : Doc
52+dot = char '.'
53+
54+backslash : Doc
55+backslash = char '\\'
56+
57+forwardslash : Doc
58+forwardslash = char '/'
59+
60+equals : Doc
61+equals = char '='
62+
63+pipe : Doc
64+pipe = char '|'
65+
66+bang : Doc
67+bang = char '!'
68+
69+tick : Doc
70+tick = char '`'
71+
72+tilda : Doc
73+tilda = char '~'
74+
75+hash : Doc
76+hash = char '#'
77+
78+asterix : Doc
79+asterix = char '*'
80+
81+ampersand : Doc
82+ampersand = char '&'
83+
84+dash : Doc
85+dash = char '-'
86+
87+question : Doc
88+question = char '?'
89+
90+dollar : Doc
91+dollar = char '$'
92+
93+pound : Doc
94+pound = char '£'
95+
96+euro : Doc
97+euro = char '€'
98+
99+caret : Doc
100+caret = char '^'
101+
102+percent : Doc
103+percent = char '%'
libs/contrib/Text/PrettyPrint/WL/Combinators.idrnew file+259
@@ -0,0 +1,259 @@
1+||| Common combinators.
2+module Text.PrettyPrint.WL.Combinators
3+
4+import Text.PrettyPrint.WL.Core
5+import Text.PrettyPrint.WL.Characters
6+
7+%default total
8+%access export
9+
10+-- --------------------------------------------------- [ Alignment Combinators ]
11+
12+||| The document `(align x)` renders document `x` with the nesting
13+||| level set to the current column. It is used for example to
14+||| implement 'hang'.
15+align : Doc -> Doc
16+align d = column (\k => nesting (\i => nest (k - i) d))
17+
18+||| The hang combinator implements hanging indentation. The document
19+||| `(hang i x)` renders document `x` with a nesting level set to the
20+||| current column plus `i`.
21+hang : Int -> Doc -> Doc
22+hang i d = align (nest i d)
23+
24+||| The document `(indent i x)` indents document `x` with `i` spaces.
25+indent : Int -> Doc -> Doc
26+indent i d = hang i (text (spaces i) <+> d)
27+
28+-- -------------------------------------------------- [ High-Level Combinators ]
29+
30+||| The document `softLine` behaves like `space` if the resulting
31+||| output fits the page, otherwise it behaves like `line`.
32+softLine : Doc
33+softLine = group line
34+
35+||| The document `softbreak` behaves like `empty` if the resulting
36+||| output fits the page, otherwise it behaves like 'line'.
37+softBreak : Doc
38+softBreak = group breakLine
39+
40+infixr 5 |/|, |//|, |$|, |$$|
41+infixr 6 |+|, |++|
42+
43+private
44+concatDoc : Doc -> Doc -> Doc -> Doc
45+concatDoc sep x y = x `beside` (sep `beside` y)
46+
47+||| The document `(x |+| y)` concatenates document `x` and document
48+||| `y`. It is an associative operation having 'empty' as a left and
49+||| right unit.
50+(|+|) : Doc -> Doc -> Doc
51+(|+|) = (<+>)
52+
53+||| The document `(x |++| y)` concatenates document `x` and `y` with a
54+||| `space` in between.
55+(|++|) : Doc -> Doc -> Doc
56+(|++|) = concatDoc space
57+
58+||| The document `(x |/| y)` concatenates document `x` and `y` with a
59+||| 'softline' in between. This effectively puts `x` and `y` either
60+||| next to each other (with a `space` in between) or underneath each
61+||| other.
62+(|/|) : Doc -> Doc -> Doc
63+(|/|) = concatDoc softLine
64+
65+||| The document `(x |//| y)` concatenates document `x` and `y` with
66+||| a 'softbreak' in between. This effectively puts `x` and `y` either
67+||| right next to each other or underneath each other.
68+(|//|) : Doc -> Doc -> Doc
69+(|//|) = concatDoc softBreak
70+
71+||| The document `(x |$| y)` concatenates document `x` and `y` with a
72+||| `line` in between.
73+(|$|) : Doc -> Doc -> Doc
74+(|$|) = concatDoc line
75+
76+||| The document `(x |$$| y)` concatenates document `x` and `y` with
77+||| a `linebreak` in between.
78+(|$$|) : Doc -> Doc -> Doc
79+(|$$|) = concatDoc breakLine
80+
81+||| The document `(vsep xs)` concatenates all documents `xs`
82+||| vertically with `(|$|)`. If a 'group' undoes the line breaks
83+||| inserted by `vsep`, all documents are separated with a space.
84+vsep : List Doc -> Doc
85+vsep = fold (|$|)
86+
87+||| The document `(sep xs)` concatenates all documents `xs` either
88+||| horizontally with `(|++|)`, if it fits the page, or vertically with
89+||| `(|$|)`.
90+sep : List Doc -> Doc
91+sep = group . vsep
92+
93+
94+||| The document `(fillSep xs)` concatenates documents `xs`
95+||| horizontally with `(|++|)` as long as its fits the page, than
96+||| inserts a `line` and continues doing that for all documents in
97+||| `xs`.
98+fillSep : List Doc -> Doc
99+fillSep = fold (|/|)
100+
101+||| The document `(hsep xs)` concatenates all documents `xs`
102+||| horizontally with `(|++|)`.
103+hsep : List Doc -> Doc
104+hsep = fold (|++|)
105+
106+||| The document `(hcat xs)` concatenates all documents `xs`
107+||| horizontally with `(|+|)`.
108+hcat : List Doc -> Doc
109+hcat = fold (<+>)
110+
111+||| The document `(vcat xs)` concatenates all documents `xs`
112+||| vertically with `(|$$|)`. If a `group` undoes the line breaks
113+||| inserted by `vcat`, all documents are directly concatenated.
114+vcat : List Doc -> Doc
115+vcat = fold (|$$|)
116+
117+||| The document `(cat xs)` concatenates all documents `xs` either
118+||| horizontally with `(|+|)`, if it fits the page, or vertically with
119+||| `(|$$|)`.
120+cat : List Doc -> Doc
121+cat = group . vcat
122+
123+||| The document `(fillCat xs)` concatenates documents `xs`
124+||| horizontally with `(|+|)` as long as its fits the page, than inserts
125+||| a `linebreak` and continues doing that for all documents in `xs`.
126+fillCat : List Doc -> Doc
127+fillCat = fold (|//|)
128+
129+||| The document `(enclose l r x)` encloses document `x` between
130+||| documents `l` and `r` using `(|+|)`.
131+enclose : Doc -> Doc -> Doc -> Doc
132+enclose l r x = concatDoc x l r
133+
134+squotes : Doc -> Doc
135+squotes = enclose squote squote
136+
137+dquotes : Doc -> Doc
138+dquotes = enclose dquote dquote
139+
140+braces : Doc -> Doc
141+braces = enclose lbrace rbrace
142+
143+parens : Doc -> Doc
144+parens = enclose lparen rparen
145+
146+angles : Doc -> Doc
147+angles = enclose langle rangle
148+
149+brackets : Doc -> Doc
150+brackets = enclose lbracket rbracket
151+
152+-- ----------------------------------------------------- [ Lists, Sets, Tuples ]
153+
154+||| The document `(encloseSep l r sep xs)` concatenates the documents
155+||| `xs` separated by `sep` and encloses the resulting document by `l`
156+||| and `r`. The documents are rendered horizontally if that fits the
157+||| page. Otherwise they are aligned vertically. All separators are put
158+||| in front of the elements.
159+encloseSep : (l : Doc)
160+ -> (r : Doc)
161+ -> (sep : Doc)
162+ -> (xs : List Doc)
163+ -> Doc
164+encloseSep l r s [] = l <+> r
165+encloseSep l r s [x] = l <+> x <+> r
166+encloseSep l r s xs = align (cat (zipWith (<+>) (l :: replicate (length xs) s) xs) <+> r)
167+
168+||| The document `(list xs)` comma separates the documents `xs` and
169+||| encloses them in square brackets. The documents are rendered
170+||| horizontally if that fits the page. Otherwise they are aligned
171+||| vertically. All comma separators are put in front of the
172+||| elements.
173+list : List Doc -> Doc
174+list = encloseSep lbracket rbracket comma
175+
176+||| The document `(tupled xs)` comma separates the documents `xs`
177+||| and encloses them in parenthesis. The documents are rendered
178+||| horizontally if that fits the page. Otherwise they are aligned
179+||| vertically. All comma separators are put in front of the
180+||| elements.
181+tupled : List Doc -> Doc
182+tupled = encloseSep lparen rparen comma
183+
184+||| The document `(set xs)` separates the documents `xs` with
185+||| commas and encloses them in braces. The documents are
186+||| rendered horizontally if that fits the page. Otherwise they are
187+||| aligned vertically. All comma's are put in front of the
188+||| elements.
189+set : List Doc -> Doc
190+set = encloseSep lbrace rbrace comma
191+
192+||| The document `(semiBraces xs)` separates the documents `xs` with
193+||| semi-colon and encloses them in braces. The documents are
194+||| rendered horizontally if that fits the page. Otherwise they are
195+||| aligned vertically. All semi-colons's are put in front of the
196+||| elements.
197+semiBrace : List Doc -> Doc
198+semiBrace = encloseSep lbrace rbrace semi
199+
200+||| `(punctuate p xs)` concatenates all documents in `xs` with
201+||| document `p` except for the last document.
202+punctuate : Doc -> List Doc -> List Doc
203+punctuate p [] = []
204+punctuate p [x] = [x]
205+punctuate p (x :: xs) = (x <+> p) :: punctuate p xs
206+
207+-- ------------------------------------------------------------------- [ Fills ]
208+
209+width : Doc -> (Int -> Doc) -> Doc
210+width doc f = column (\k => doc <+> column (\k' => f (k' - k)))
211+
212+||| The document `(fillBreak i x)` first renders document `x`. It
213+||| than appends `space`s until the width is equal to `i`. If the
214+||| width of `x` is already larger than `i`, the nesting level is
215+||| increased by `i` and a `line` is appended.
216+fillBreak : (i : Int) -> (x : Doc) -> Doc
217+fillBreak f x =
218+ width x (\w => if (w > f)
219+ then nest f breakLine
220+ else text (spaces (f - w)))
221+
222+||| The document `(fill i x)` renders document `x`. It than appends
223+||| `space`s until the width is equal to `i`. If the width of `x` is
224+||| already larger, nothing is appended. This combinator is quite
225+||| useful in practice to output a list of bindings.
226+fill : (i : Int) -> (x : Doc) -> Doc
227+fill f d =
228+ width d (\w => if (w >= f)
229+ then empty
230+ else text (spaces (f - w)))
231+
232+-- -------------------------------------------------------------- [ Primatives ]
233+
234+||| The document `(literal s)` concatenates all characters in `s`
235+||| using `line` for newline characters and `char` for all other
236+||| characters. It is used instead of 'text' whenever the text contains
237+||| newline characters.
238+literal : (str : String) -> Doc
239+literal str = mkLiteral (unpack str)
240+ where
241+ mkLiteral : List Char -> Doc
242+ mkLiteral Nil = empty
243+ mkLiteral ('\n':: ss) = line <+> mkLiteral ss
244+ mkLiteral (c :: ss) = char c <+> mkLiteral ss
245+
246+bool : Bool -> Doc
247+bool b = text (show b)
248+
249+nat : Nat -> Doc
250+nat n = text (show n)
251+
252+int : Int -> Doc
253+int i = text (show i)
254+
255+integer : Integer -> Doc
256+integer i = text (show i)
257+
258+double : Double -> Doc
259+double d = text (show d)
libs/contrib/Text/PrettyPrint/WL/Core.idrnew file+225
@@ -0,0 +1,225 @@
1+||| Core definitions and primitives.
2+module Text.PrettyPrint.WL.Core
3+
4+%default total
5+%access export
6+
7+-- -------------------------------------------------------------------- [ Core ]
8+
9+||| The abstract data type `Doc` represents pretty documents.
10+|||
11+data Doc : Type where
12+ Empty : Doc
13+ Chara : (c : Char) -> Doc
14+ Text : (len : Int) -> (str : String) -> Doc
15+ Line : (undone : Bool) -> Doc
16+
17+ Cat : (x : Doc) -> (y : Doc) -> Doc
18+ Nest : (lvl : Int) -> (x : Doc) -> Doc
19+ Union : (x : Doc) -> (y : Doc) -> Doc
20+
21+ Column : (f : Int -> Doc) -> Doc
22+ Nesting : (f : Int -> Doc) -> Doc
23+
24+-- -------------------------------------------------------------- [ Primitives ]
25+
26+||| The empty document is, indeed, empty.
27+empty : Doc
28+empty = Empty
29+
30+||| The `line` document advances to the next line and indents to the
31+||| current nesting level. Document `line` behaves like `(text " ")`
32+||| if the line break is undone by 'group'.
33+line : Doc
34+line = Line False
35+
36+||| The document `(char c)` contains the literal character `c`. If the
37+||| character is a newline (`'\n'`) the function returns a line
38+||| document. Ideally, the function 'line' should be used for line
39+||| breaks.
40+char : (c : Char) -> Doc
41+char '\n' = line
42+char c = Chara c
43+
44+||| The document `(text s)` contains the literal string `s`. The
45+||| string shouldn't contain any newline (`'\n'`) characters. If the
46+||| string contains newline characters, the function 'literal' should be
47+||| used.
48+text : (str : String) -> Doc
49+text "" = empty
50+text str = Text (cast $ length str) str
51+
52+||| The `breakLine` document advances to the next line and indents to
53+||| the current nesting level. Document `breakLine` behaves like
54+||| 'empty' if the line break is undone by 'group'.
55+breakLine : Doc
56+breakLine = Line True
57+
58+||| Horizontal concatenation of documents
59+beside : Doc -> Doc -> Doc
60+beside = Cat
61+
62+||| The document `(nest lvl x)` renders document `x` with the current
63+||| indentation level increased by lvl.
64+nest : (lvl : Int)
65+ -> (x : Doc)
66+ -> Doc
67+nest = Nest
68+
69+column : (f : Int -> Doc) -> Doc
70+column = Column
71+
72+nesting : (f : Int -> Doc) -> Doc
73+nesting = Nesting
74+
75+private %inline
76+flatten : Doc -> Doc
77+flatten (Line break) = if break then Empty else Text 1 " "
78+
79+flatten (Cat x y) = Cat (flatten x) (flatten y)
80+flatten (Nest lvl x) = Nest lvl (flatten x)
81+flatten (Union x _) = flatten x
82+flatten (Column f) = Column (\i => flatten $ f i)
83+flatten (Nesting f) = Nesting (\i => flatten $ f i)
84+
85+flatten other = other
86+
87+||| The `group` combinator is used to specify alternative
88+||| layouts. The document `(group x)` undoes all line breaks in
89+||| document `x`. The resulting line is added to the current line if
90+||| that fits the page. Otherwise, the document `x` is rendered without
91+||| any changes.
92+group : Doc -> Doc
93+group x = Union (flatten x) x
94+
95+Semigroup Doc where
96+ (<+>) x y = beside x y
97+
98+Monoid Doc where
99+ neutral = empty
100+
101+fold : (f : Doc -> Doc -> Doc) -> (ds : List Doc) -> Doc
102+fold _ Nil = empty
103+fold f (x::xs) = foldl f x xs
104+
105+-- --------------------------------------------------------------- [ Renderers ]
106+
107+namespace PrettyDoc
108+
109+ ||| The data type `PrettyDoc` represents rendered documents and is
110+ ||| used by the display functions.
111+ data PrettyDoc : Type where
112+ Empty : PrettyDoc
113+ Chara : (c : Char) -> (rest : PrettyDoc) -> PrettyDoc
114+ Text : (len : Int) -> (str : String) -> (rest : PrettyDoc) -> PrettyDoc
115+ Line : (lvl : Int) -> (rest : PrettyDoc) -> PrettyDoc
116+
117+||| Helper function to construct spaces.
118+spaces : (n : Int) -> String
119+spaces n = if n <= 0 then "" else pack $ replicate (cast n) ' '
120+
121+private
122+indentation : Int -> String
123+indentation n = spaces n
124+
125+||| `(showPrettyDoc doc)` takes the output `PrettyDoc` from a
126+||| rendering function and transforms it to a String for printing.
127+showPrettyDoc : (doc : PrettyDoc) -> String
128+showPrettyDoc doc = showPrettyDocS doc ""
129+ where
130+ showPrettyDocS : (doc : PrettyDoc) -> (acc : String) -> String
131+ showPrettyDocS Empty = id
132+ showPrettyDocS (Chara c rest) = strCons c . showPrettyDocS rest
133+ showPrettyDocS (Text len str rest) = (str ++) . showPrettyDocS rest
134+ showPrettyDocS (Line lvl rest) = (('\n' `strCons` indentation lvl) ++) . showPrettyDocS rest
135+
136+private
137+fits : (w : Int) -> (x : PrettyDoc) -> Bool
138+fits w Empty = if w < 0 then False else True
139+fits w (Chara c rest) = if w < 0 then False else fits (w - 1) rest
140+
141+fits w (Text len str rest) = if w < 0 then False else fits (w - len) rest
142+
143+fits w (Line _ _) = if w < 0 then False else True
144+
145+
146+||| Use the Wadler-Leijen algorithm to pretty print the `doc`.
147+||| The algorithm uses a page width of `width` and a ribbon
148+||| width of `(ribbonfrac * width)` characters. The ribbon width is
149+||| the maximal amount of non-indentation characters on a line. The
150+||| parameter `ribbonfrac` should be between `0.0` and `1.0`. If it is
151+||| lower or higher, the ribbon width will be 0 or `width`
152+||| respectively.
153+render : (rfrac : Double)
154+ -> (width : Int)
155+ -> (doc : Doc)
156+ -> PrettyDoc
157+render rfrac w doc = best w 0 0 doc (const Empty)
158+ where
159+ rwidth : Int
160+ rwidth = max 0 $ min w (cast (cast w * rfrac))
161+
162+ nicest : (lvl : Int)
163+ -> (col : Int)
164+ -> (x : PrettyDoc)
165+ -> (y : PrettyDoc)
166+ -> PrettyDoc
167+ nicest n k x y =
168+ let width = min (w - k) (rwidth - k + n)
169+ in if fits width x then x else y
170+
171+ best : (lvl : Int)
172+ -> (col : Int)
173+ -> (curr : Int)
174+ -> (doc : Doc)
175+ -> (k : Int -> PrettyDoc)
176+ -> PrettyDoc
177+ best lvl col curr Empty k = k col
178+ best lvl col curr (Chara c) k = Chara c $ k (col + 1)
179+ best lvl col curr (Text len str) k = Text len str $ k (col + len)
180+ best lvl col curr (Line undone) k = Line curr $ k curr
181+
182+ best lvl col curr (Cat x y) k =
183+ best lvl col curr x (\curr' => best lvl curr' curr y k)
184+
185+ best lvl col curr (Nest x y) k = best lvl col (curr+x) y k
186+
187+ best lvl col curr (Union x y) k =
188+ nicest lvl col (best lvl col curr x k)
189+ (best lvl col curr y k)
190+
191+ best lvl col curr (Column f) k = best lvl col curr (f col) k
192+ best lvl col curr (Nesting f) k = best lvl col curr (f curr) k
193+
194+||| Print the document to a string using the given ribbon fraction
195+||| and page width.
196+toString : (rfrac : Double)
197+ -> (width : Int)
198+ -> (doc : Doc)
199+ -> String
200+toString rfrac width doc = showPrettyDoc (render rfrac width doc)
201+
202+writeDoc : (fname : String)
203+ -> (rfrac : Double)
204+ -> (width : Int)
205+ -> (doc : Doc)
206+ -> IO (Either FileError ())
207+writeDoc fname rfrac width doc = writeFile fname $ toString rfrac width doc
208+
209+namespace Default
210+
211+ ||| Render the document with a default ribbon fraction of 0.4 and page width of 120 characters.
212+ render : (doc : Doc) -> PrettyDoc
213+ render = render 0.4 120
214+
215+ ||| Print the document to a string using a default ribbon fraction
216+ ||| of 0.4 and page width of 120 characters.
217+ toString : (doc : Doc) -> String
218+ toString = toString 0.4 120
219+
220+ ||| Write the doc to `fname` using a default ribbon fraction of 0.4
221+ ||| and page width of 120 characters.
222+ writeDoc : (fname : String)
223+ -> (doc : Doc)
224+ -> IO (Either FileError ())
225+ writeDoc fname doc = writeFile fname $ Default.toString doc
libs/contrib/contrib.ipkg+7
@@ -30,4 +30,11 @@ modules = CFFI, CFFI.Types, CFFI.Memory,
3030
3131 System.Concurrency.Process,
3232
33+ Text.Lexer, Text.Parser,
34+
35+ Text.PrettyPrint.WL,
36+ Text.PrettyPrint.WL.Core,
37+ Text.PrettyPrint.WL.Characters,
38+ Text.PrettyPrint.WL.Combinators,
39+
3340 Data.Fin.Extra
libs/prelude/Decidable/Equality.idr+15−9
@@ -8,18 +8,10 @@ import Prelude.Either
88import Prelude.List
99import Prelude.Nat
1010import Prelude.Maybe
11+import Prelude.Uninhabited
1112
1213%access public export
1314
14−--------------------------------------------------------------------------------
15−-- Utility lemmas
16−--------------------------------------------------------------------------------
17−
18−||| The negation of equality is symmetric (follows from symmetry of equality)
19−total negEqSym : {a : t} -> {b : t} -> (a = b -> Void) -> (b = a -> Void)
20−negEqSym p h = p (sym h)
21−
22−
2315--------------------------------------------------------------------------------
2416-- Decidable equality
2517--------------------------------------------------------------------------------
@@ -29,6 +21,20 @@ interface DecEq t where
2921 ||| Decide whether two elements of `t` are propositionally equal
3022 total decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
3123
24+--------------------------------------------------------------------------------
25+-- Utility lemmas
26+--------------------------------------------------------------------------------
27+
28+||| The negation of equality is symmetric (follows from symmetry of equality)
29+total negEqSym : {a : t} -> {b : t} -> (a = b -> Void) -> (b = a -> Void)
30+negEqSym p h = p (sym h)
31+
32+||| Everything is decidably equal to itself
33+total decEqSelfIsYes : DecEq a => {x : a} -> decEq x x = Yes Refl
34+decEqSelfIsYes {x} with (decEq x x)
35+ | Yes Refl = Refl
36+ | No contra = absurd $ contra Refl
37+
3238--------------------------------------------------------------------------------
3339--- Unit
3440--------------------------------------------------------------------------------
libs/prelude/Prelude/Bool.idr+9
@@ -35,3 +35,12 @@ not : Bool -> Bool
3535not True = False
3636not False = True
3737
38+--------------------------------------------------------------------------------
39+-- Properties
40+--------------------------------------------------------------------------------
41+
42+Uninhabited (True = False) where
43+ uninhabited Refl impossible
44+
45+Uninhabited (False = True) where
46+ uninhabited Refl impossible
libs/prelude/Prelude/Cast.idr+1−1
@@ -7,7 +7,7 @@ import public Builtins
77
88||| Interface for transforming an instance of a data type to another type.
99interface Cast from to where
10− ||| Perform a cast operation.
10+ ||| Perform a (potentially lossy!) cast operation.
1111 |||
1212 ||| @orig The original type.
1313 cast : (orig : from) -> to
libs/prelude/Prelude/Doubles.idr+3
@@ -21,6 +21,9 @@ exp x = prim__floatExp x
2121log : Double -> Double
2222log x = prim__floatLog x
2323
24+pow : Double -> Double -> Double
25+pow x y = exp (y * log x)
26+
2427sin : Double -> Double
2528sin x = prim__floatSin x
2629
libs/prelude/Prelude/List.idr+5−1
@@ -378,7 +378,7 @@ scanl : (b -> a -> b) -> b -> List a -> List b
378378scanl f q [] = [q]
379379scanl f q (x::xs) = q :: scanl f (f q x) xs
380380
381−||| The scanl1 function is a variant of scanl that doesn't require an explicit
381+||| The scanl1 function is a variant of scanl that doesn't require an explicit
382382||| starting value.
383383||| It assumes the first element of the list to be the starting value and then
384384||| starts the fold with the element following it.
@@ -855,6 +855,10 @@ catMaybes (x::xs) =
855855-- Properties
856856--------------------------------------------------------------------------------
857857
858+||| (::) is injective
859+consInjective : (x :: xs) = (y :: ys) -> (x = y, xs = ys)
860+consInjective Refl = (Refl, Refl)
861+
858862||| The empty list is a right identity for append.
859863appendNilRightNeutral : (l : List a) ->
860864 l ++ [] = l
libs/prelude/Prelude/Monad.idr+6−1
@@ -6,6 +6,7 @@ import Builtins
66import Prelude.Functor
77import public Prelude.Applicative
88import Prelude.Basics
9+import Prelude.Foldable
910import IO
1011
1112%access public export
@@ -33,6 +34,11 @@ flatten : Monad m => m (m a) -> m a
3334flatten = join
3435%deprecate flatten "Please use `join`, which is the standard name."
3536
37+||| Similar to `foldl`, but uses a function wrapping its result in a `Monad`.
38+||| Consequently, the final value is wrapped in the same `Monad`.
39+foldlM : (Foldable t, Monad m) => (funcM: a -> b -> m a) -> (init: a) -> (input: t b) -> m a
40+foldlM fm a0 = foldl (\ma,b => ma >>= flip fm b) (pure a0)
41+
3642-- Annoyingly, these need to be here, so that we can use them in other
3743-- Prelude modules other than the top level.
3844
@@ -48,4 +54,3 @@ Applicative (IO' ffi) where
4854
4955Monad (IO' ffi) where
5056 b >>= k = io_bind b k
51−
libs/prelude/Prelude/Nat.idr+2−5
@@ -191,13 +191,10 @@ maximum Z m = m
191191maximum (S n) Z = S n
192192maximum (S n) (S m) = S (maximum n m)
193193
194−||| Tail recursive cast Nat to Int
194+||| Cast Nat to Int
195195||| Note that this can overflow
196196toIntNat : Nat -> Int
197−toIntNat n = toIntNat' n 0 where
198− toIntNat' : Nat -> Int -> Int
199− toIntNat' Z x = x
200− toIntNat' (S n) x = toIntNat' n (x + 1)
197+toIntNat n = prim__truncBigInt_Int (toIntegerNat n)
201198
202199(-) : (m : Nat) -> (n : Nat) -> {auto smaller : LTE n m} -> Nat
203200(-) m n {smaller} = minus m n
libs/prelude/Prelude/WellFounded.idr+40−22
@@ -85,28 +85,46 @@ wfInd : WellFounded rel => {P : a -> Type} ->
8585 (x : a) -> P x
8686wfInd {rel} step x = accInd step x (wellFounded {rel} x)
8787
88−-- Some basic useful relations
88+||| Interface of types with sized values.
89+||| The size is used for proofs of termination via accessibility.
90+|||
91+||| @ a the type whose elements can be mapped to Nat
92+interface Sized a where
93+ size : a -> Nat
8994
90−||| LT is a well-founded relation on numbers
91−ltAccessible : (n : Nat) -> Accessible LT n
92−ltAccessible n = Access (\v, prf => ltAccessible' {n'=v} n prf)
93− where
94− ltAccessible' : (m : Nat) -> LT n' m -> Accessible LT n'
95− ltAccessible' Z x = absurd x
96− ltAccessible' (S k) (LTESucc x)
97− = Access (\val, p => ltAccessible' k (lteTransitive p x))
98−
99−-- First list is smaller than the second
100−smaller : List a -> List a -> Type
101−smaller xs ys = LT (length xs) (length ys)
102−
103−||| `smaller` is a well-founded relation on lists
104−smallerAcc : (xs : List a) -> Accessible WellFounded.smaller xs
105−smallerAcc xs = Access (\v, prf => smallerAcc' {xs'=v} xs prf)
106− where
107− smallerAcc' : (ys : List a) -> smaller xs' ys -> Accessible smaller xs'
108− smallerAcc' [] x = absurd x
109− smallerAcc' (y :: ys) (LTESucc x)
110− = Access (\val, p => smallerAcc' ys (lteTransitive p x))
95+Smaller : Sized a => a -> a -> Type
96+Smaller x y = size x `LT` size y
11197
98+SizeAccessible : Sized a => a -> Type
99+SizeAccessible = Accessible Smaller
112100
101+||| Proof of well-foundedness of `Smaller`.
102+||| Constructs accessibility for any given element of `a`, provided `Sized a`.
103+sizeAccessible : Sized a => (x : a) -> SizeAccessible x
104+sizeAccessible x = Access (acc $ size x)
105+ where
106+ acc : (sizeX : Nat) -> (y : a) -> (size y `LT` sizeX) -> SizeAccessible y
107+ acc (S x') y (LTESucc yLEx')
108+ = Access (\z, zLTy => acc x' z (lteTransitive zLTy yLEx'))
109+
110+||| Strong induction principle for sized types.
111+sizeInd : Sized a
112+ => {P : a -> Type}
113+ -> (step : (x : a) -> ((y : a) -> Smaller y x -> P y) -> P x)
114+ -> (z : a)
115+ -> P z
116+sizeInd step z = accInd step z (sizeAccessible z)
117+
118+||| Strong recursion principle for sized types.
119+sizeRec : Sized a
120+ => (step : (x : a) -> ((y : a) -> Smaller y x -> b) -> b)
121+ -> (z : a)
122+ -> b
123+sizeRec step z = accRec step z (sizeAccessible z)
124+
125+
126+implementation Sized Nat where
127+ size = \x => x
128+
129+implementation Sized (List a) where
130+ size = length
main/Main.hs+1
@@ -11,6 +11,7 @@ import Idris.CmdOptions
1111import Idris.Error
1212import Idris.Info.Show
1313import Idris.Main
14+import Idris.Options
1415import Idris.Package
1516
1617import Util.System (setupBundledCC)
rts/idris_gc.c+1−1
@@ -24,7 +24,7 @@ VAL copy(VM* vm, VAL x) {
2424 cl = MKFLOATc(vm, x->info.f);
2525 break;
2626 case CT_STRING:
27− cl = MKSTRc(vm, x->info.str);
27+ cl = MKSTRclen(vm, x->info.str.str, x->info.str.len);
2828 break;
2929 case CT_STROFFSET:
3030 cl = MKSTROFFc(vm, x->info.str_offset);
rts/idris_gmp.h+2
@@ -7,6 +7,8 @@
77#include "mini-gmp.h"
88#endif
99
10+#include "idris_rts.h"
11+
1012// Set memory allocation functions
1113void init_gmpalloc(void);
1214
rts/idris_main.c+1
@@ -3,6 +3,7 @@
33#include "idris_rts.h"
44#include "idris_stats.h"
55
6+void _idris__123_runMain_95_0_125_(VM* vm, VAL* oldbase);
67#if defined(WIN32) || defined(__WIN32) || defined(__WIN32__)
78#include <Windows.h>
89int win32_get_argv_utf8(int *argc_ptr, char ***argv_ptr)
rts/idris_rts.c+86−42
@@ -285,19 +285,27 @@ VAL MKSTR(VM* vm, const char* str) {
285285 Closure* cl = allocate(sizeof(Closure) + // Type) + sizeof(char*) +
286286 sizeof(char)*len, 0);
287287 SETTY(cl, CT_STRING);
288− cl -> info.str = (char*)cl + sizeof(Closure);
288+ cl->info.str.str = (char*)cl + sizeof(Closure);
289289 if (str == NULL) {
290− cl->info.str = NULL;
290+ cl->info.str.str = NULL;
291291 } else {
292− strcpy(cl -> info.str, str);
292+ strcpy(cl->info.str.str, str);
293293 }
294+ cl->info.str.len = len > 0 ? len : 0;
294295 return cl;
295296}
296297
297298char* GETSTROFF(VAL stroff) {
298299 // Assume STROFF
299300 StrOffset* root = stroff->info.str_offset;
300− return (root->str->info.str + root->offset);
301+ return (root->str->info.str.str + root->offset);
302+}
303+
304+size_t GETSTROFFLEN(VAL stroff) {
305+ // Assume STROFF
306+ // we're working in char* here so no worries about utf8 char length
307+ StrOffset* root = stroff->info.str_offset;
308+ return (root->str->info.str.len - root->offset);
301309}
302310
303311VAL MKCDATA(VM* vm, CHeapItem * item) {
@@ -342,12 +350,26 @@ VAL MKFLOATc(VM* vm, double val) {
342350}
343351
344352VAL MKSTRc(VM* vm, char* str) {
353+ int len = strlen(str);
354+
355+ Closure* cl = allocate(sizeof(Closure) + // Type) + sizeof(char*) +
356+ sizeof(char)*len+1, 1);
357+ SETTY(cl, CT_STRING);
358+ cl -> info.str.str = (char*)cl + sizeof(Closure);
359+
360+ strcpy(cl->info.str.str, str);
361+ cl->info.str.len = len;
362+ return cl;
363+}
364+
365+VAL MKSTRclen(VM* vm, char* str, int len) {
345366 Closure* cl = allocate(sizeof(Closure) + // Type) + sizeof(char*) +
346− sizeof(char)*strlen(str)+1, 1);
367+ sizeof(char)*len+1, 1);
347368 SETTY(cl, CT_STRING);
348− cl -> info.str = (char*)cl + sizeof(Closure);
369+ cl -> info.str.str = (char*)cl + sizeof(Closure);
349370
350− strcpy(cl -> info.str, str);
371+ strcpy(cl->info.str.str, str);
372+ cl->info.str.len = len;
351373 return cl;
352374}
353375
@@ -397,6 +419,13 @@ VAL MKB64(VM* vm, uint64_t bits64) {
397419 return cl;
398420}
399421
422+void idris_trace(VM* vm, const char* func, int line) {
423+ printf("At %s:%d\n", func, line);
424+ dumpStack(vm);
425+ puts("");
426+ fflush(stdout);
427+}
428+
400429void dumpStack(VM* vm) {
401430 int i = 0;
402431 VAL* root;
@@ -404,7 +433,8 @@ void dumpStack(VM* vm) {
404433 for (root = vm->valstack; root < vm->valstack_top; ++root, ++i) {
405434 printf("%d: ", i);
406435 dumpVal(*root);
407− if (*root >= (VAL)(vm->heap.heap) && *root < (VAL)(vm->heap.end)) { printf("OK"); }
436+ if (*root >= (VAL)(vm->heap.heap) && *root < (VAL)(vm->heap.end)) { printf(" OK"); }
437+ if (root == vm->valstack_base) { printf(" <--- base"); }
408438 printf("\n");
409439 }
410440 printf("RET: ");
@@ -428,7 +458,7 @@ void dumpVal(VAL v) {
428458 printf("] ");
429459 break;
430460 case CT_STRING:
431− printf("STR[%s]", v->info.str);
461+ printf("STR[%s]", v->info.str.str);
432462 break;
433463 case CT_FWD:
434464 printf("CT_FWD ");
@@ -490,8 +520,9 @@ VAL idris_castIntStr(VM* vm, VAL i) {
490520 int x = (int) GETINT(i);
491521 Closure* cl = allocate(sizeof(Closure) + sizeof(char)*16, 0);
492522 SETTY(cl, CT_STRING);
493− cl -> info.str = (char*)cl + sizeof(Closure);
494− sprintf(cl -> info.str, "%d", x);
523+ cl->info.str.str = (char*)cl + sizeof(Closure);
524+ sprintf(cl->info.str.str, "%d", x);
525+ cl->info.str.len = strlen(cl->info.str.str);
495526 return cl;
496527}
497528
@@ -503,32 +534,33 @@ VAL idris_castBitsStr(VM* vm, VAL i) {
503534 case CT_BITS8:
504535 // max length 8 bit unsigned int str 3 chars (256)
505536 cl = allocate(sizeof(Closure) + sizeof(char)*4, 0);
506− cl->info.str = (char*)cl + sizeof(Closure);
507− sprintf(cl->info.str, "%" PRIu8, (uint8_t)i->info.bits8);
537+ cl->info.str.str = (char*)cl + sizeof(Closure);
538+ sprintf(cl->info.str.str, "%" PRIu8, (uint8_t)i->info.bits8);
508539 break;
509540 case CT_BITS16:
510541 // max length 16 bit unsigned int str 5 chars (65,535)
511542 cl = allocate(sizeof(Closure) + sizeof(char)*6, 0);
512− cl->info.str = (char*)cl + sizeof(Closure);
513− sprintf(cl->info.str, "%" PRIu16, (uint16_t)i->info.bits16);
543+ cl->info.str.str = (char*)cl + sizeof(Closure);
544+ sprintf(cl->info.str.str, "%" PRIu16, (uint16_t)i->info.bits16);
514545 break;
515546 case CT_BITS32:
516547 // max length 32 bit unsigned int str 10 chars (4,294,967,295)
517548 cl = allocate(sizeof(Closure) + sizeof(char)*11, 0);
518− cl->info.str = (char*)cl + sizeof(Closure);
519− sprintf(cl->info.str, "%" PRIu32, (uint32_t)i->info.bits32);
549+ cl->info.str.str = (char*)cl + sizeof(Closure);
550+ sprintf(cl->info.str.str, "%" PRIu32, (uint32_t)i->info.bits32);
520551 break;
521552 case CT_BITS64:
522553 // max length 64 bit unsigned int str 20 chars (18,446,744,073,709,551,615)
523554 cl = allocate(sizeof(Closure) + sizeof(char)*21, 0);
524− cl->info.str = (char*)cl + sizeof(Closure);
525− sprintf(cl->info.str, "%" PRIu64, (uint64_t)i->info.bits64);
555+ cl->info.str.str = (char*)cl + sizeof(Closure);
556+ sprintf(cl->info.str.str, "%" PRIu64, (uint64_t)i->info.bits64);
526557 break;
527558 default:
528559 fprintf(stderr, "Fatal Error: ClosureType %d, not an integer type", ty);
529560 exit(EXIT_FAILURE);
530561 }
531562
563+ cl->info.str.len = strlen(cl->info.str.str);
532564 SETTY(cl, CT_STRING);
533565 return cl;
534566}
@@ -545,8 +577,10 @@ VAL idris_castStrInt(VM* vm, VAL i) {
545577VAL idris_castFloatStr(VM* vm, VAL i) {
546578 Closure* cl = allocate(sizeof(Closure) + sizeof(char)*32, 0);
547579 SETTY(cl, CT_STRING);
548− cl -> info.str = (char*)cl + sizeof(Closure);
549− snprintf(cl -> info.str, 32, "%.16g", GETFLOAT(i));
580+ cl->info.str.str = (char*)cl + sizeof(Closure);
581+ snprintf(cl->info.str.str, 32, "%.16g", GETFLOAT(i));
582+
583+ cl->info.str.len = strlen(cl->info.str.str);
550584 return cl;
551585}
552586
@@ -559,11 +593,13 @@ VAL idris_concat(VM* vm, VAL l, VAL r) {
559593 char *ls = GETSTR(l);
560594 // dumpVal(l);
561595 // printf("\n");
562− Closure* cl = allocate(sizeof(Closure) + strlen(ls) + strlen(rs) + 1, 0);
596+ Closure* cl = allocate(sizeof(Closure) + GETSTRLEN(l) + GETSTRLEN(r) + 1, 0);
563597 SETTY(cl, CT_STRING);
564− cl -> info.str = (char*)cl + sizeof(Closure);
565− strcpy(cl -> info.str, ls);
566− strcat(cl -> info.str, rs);
598+ cl->info.str.str = (char*)cl + sizeof(Closure);
599+ strcpy(cl->info.str.str, ls);
600+ strcat(cl->info.str.str, rs);
601+
602+ cl->info.str.len = GETSTRLEN(l) + GETSTRLEN(r);
567603 return cl;
568604}
569605
@@ -670,21 +706,26 @@ VAL idris_strTail(VM* vm, VAL str) {
670706VAL idris_strCons(VM* vm, VAL x, VAL xs) {
671707 char *xstr = GETSTR(xs);
672708 int xval = GETINT(x);
709+ int xlen = GETSTRLEN(xs);
710+
673711 if ((xval & 0x80) == 0) { // ASCII char
674712 Closure* cl = allocate(sizeof(Closure) +
675− strlen(xstr) + 2, 0);
713+ xlen + 2, 0);
676714 SETTY(cl, CT_STRING);
677− cl -> info.str = (char*)cl + sizeof(Closure);
678− cl -> info.str[0] = (char)(GETINT(x));
679− strcpy(cl -> info.str+1, xstr);
715+ cl->info.str.str = (char*)cl + sizeof(Closure);
716+ cl->info.str.str[0] = (char)(GETINT(x));
717+ strcpy(cl->info.str.str+1, xstr);
718+ cl->info.str.len = xlen + 1;
680719 return cl;
681720 } else {
682721 char *init = idris_utf8_fromChar(xval);
683− Closure* cl = allocate(sizeof(Closure) + strlen(init) + strlen(xstr) + 1, 0);
722+ int newlen = strlen(init) + xlen;
723+ Closure* cl = allocate(sizeof(Closure) + newlen + 1, 0);
684724 SETTY(cl, CT_STRING);
685− cl -> info.str = (char*)cl + sizeof(Closure);
686− strcpy(cl -> info.str, init);
687− strcat(cl -> info.str, xstr);
725+ cl->info.str.str = (char*)cl + sizeof(Closure);
726+ strcpy(cl->info.str.str, init);
727+ strcat(cl->info.str.str, xstr);
728+ cl->info.str.len = newlen;
688729 free(init);
689730 return cl;
690731 }
@@ -701,7 +742,7 @@ VAL idris_substr(VM* vm, VAL offset, VAL length, VAL str) {
701742 char* str_val = GETSTR(str);
702743
703744 // If the substring is a suffix, use idris_strShift to avoid reallocating
704− if (offset_val + length_val >= strlen(str_val)) {
745+ if (offset_val + length_val >= GETSTRLEN(str)) {
705746 return idris_strShift(vm, str, offset_val);
706747 }
707748 else {
@@ -709,20 +750,23 @@ VAL idris_substr(VM* vm, VAL offset, VAL length, VAL str) {
709750 char *end = idris_utf8_advance(start, length_val);
710751 Closure* newstr = allocate(sizeof(Closure) + (end - start) +1, 0);
711752 SETTY(newstr, CT_STRING);
712− newstr -> info.str = (char*)newstr + sizeof(Closure);
713− memcpy(newstr -> info.str, start, end - start);
714− *(newstr -> info.str + (end - start) + 1) = '\0';
753+ newstr->info.str.str = (char*)newstr + sizeof(Closure);
754+ memcpy(newstr->info.str.str, start, end - start);
755+ *(newstr->info.str.str + (end - start) + 1) = '\0';
756+ newstr->info.str.len = strlen(newstr->info.str.str);
715757 return newstr;
716758 }
717759}
718760
719761VAL idris_strRev(VM* vm, VAL str) {
720762 char *xstr = GETSTR(str);
721− Closure* cl = allocate(sizeof(Closure) +
722− strlen(xstr) + 1, 0);
763+ int xlen = GETSTRLEN(str);
764+
765+ Closure* cl = allocate(sizeof(Closure) + xlen + 1, 0);
723766 SETTY(cl, CT_STRING);
724− cl->info.str = (char*)cl + sizeof(Closure);
725− idris_utf8_rev(xstr, cl->info.str);
767+ cl->info.str.str = (char*)cl + sizeof(Closure);
768+ cl->info.str.len = xlen;
769+ idris_utf8_rev(xstr, cl->info.str.str);
726770 return cl;
727771}
728772
@@ -832,7 +876,7 @@ VAL doCopyTo(VM* vm, VAL x) {
832876 cl = MKFLOATc(vm, x->info.f);
833877 break;
834878 case CT_STRING:
835− cl = MKSTRc(vm, x->info.str);
879+ cl = MKSTRc(vm, x->info.str.str);
836880 break;
837881 case CT_BIGINT:
838882 cl = MKBIGMc(vm, x->info.ptr);
rts/idris_rts.h+20−3
@@ -42,6 +42,11 @@ typedef struct {
4242 size_t offset;
4343} StrOffset;
4444
45+typedef struct {
46+ char* str;
47+ size_t len; // Cached strlen (we do 'strlen' a lot)
48+} String;
49+
4550// A foreign pointer, managed by the idris GC
4651typedef struct {
4752 size_t size;
@@ -59,7 +64,7 @@ typedef struct Closure {
5964 con c;
6065 int i;
6166 double f;
62− char* str;
67+ String str;
6368 StrOffset* str_offset;
6469 void* ptr;
6570 uint8_t bits8;
@@ -182,7 +187,8 @@ typedef void(*func)(VM*, VAL*);
182187#define ALIGN(__p, __alignment) ((__p + __alignment - 1) & ~(__alignment - 1))
183188
184189// Retrieving values
185−#define GETSTR(x) (ISSTR(x) ? (((VAL)(x))->info.str) : GETSTROFF(x))
190+#define GETSTR(x) (ISSTR(x) ? (((VAL)(x))->info.str.str) : GETSTROFF(x))
191+#define GETSTRLEN(x) (ISSTR(x) ? (((VAL)(x))->info.str.len) : GETSTROFFLEN(x))
186192#define GETPTR(x) (((VAL)(x))->info.ptr)
187193#define GETMPTR(x) (((VAL)(x))->info.mptr->data)
188194#define GETFLOAT(x) (((VAL)(x))->info.f)
@@ -229,7 +235,15 @@ typedef intptr_t i_int;
229235
230236// Stack management
231237
232−#define INITFRAME VAL* myoldbase
238+#ifdef IDRIS_TRACE
239+#define TRACE idris_trace(vm, __FUNCTION__, __LINE__);
240+#else
241+#define TRACE
242+#endif
243+
244+#define INITFRAME TRACE\
245+ VAL* myoldbase
246+
233247#define REBASE vm->valstack_base = oldbase
234248#define RESERVE(x) if (vm->valstack_top+(x) > vm->stack_max) { stackOverflow(); } \
235249 else { memset(vm->valstack_top, 0, (x)*sizeof(VAL)); }
@@ -255,11 +269,13 @@ VAL MKCDATA(VM* vm, CHeapItem * item);
255269VAL MKFLOATc(VM* vm, double val);
256270VAL MKSTROFFc(VM* vm, StrOffset* off);
257271VAL MKSTRc(VM* vm, char* str);
272+VAL MKSTRclen(VM* vm, char* str, int len);
258273VAL MKPTRc(VM* vm, void* ptr);
259274VAL MKMPTRc(VM* vm, void* ptr, size_t size);
260275VAL MKCDATAc(VM* vm, CHeapItem * item);
261276
262277char* GETSTROFF(VAL stroff);
278+size_t GETSTROFFLEN(VAL stroff);
263279
264280// #define SETTAG(x, a) (x)->info.c.tag = (a)
265281#define SETARG(x, i, a) ((x)->info.c.args)[i] = ((VAL)(a))
@@ -340,6 +356,7 @@ VM* idris_getSender(Msg* msg);
340356int idris_getChannel(Msg* msg);
341357void idris_freeMsg(Msg* msg);
342358
359+void idris_trace(VM* vm, const char* func, int line);
343360void dumpVal(VAL r);
344361void dumpStack(VM* vm);
345362
scripts/runidrisnew file+18
@@ -0,0 +1,18 @@
1+#!/bin/sh
2+
3+# This is a script that runs an idris program, suitable for use
4+# in a shebang line. We cache the executables by naming them after
5+# the SHA hash of the idris source and looking for it before
6+# compiling
7+RUNIDRIS_DIR="${TEMP:-/tmp}/runidris"
8+if [ ! -d $RUNIDRIS_DIR ]; then
9+ mkdir $RUNIDRIS_DIR
10+ chmod 700 $RUNIDRIS_DIR
11+fi
12+TEMP_NAME="runidris-`sha1sum $1 | cut -c1-40`"
13+FP="$RUNIDRIS_DIR/$TEMP_NAME"
14+if [ ! -e $FP ]; then
15+ "${IDRIS:-idris}" $1 --ibcsubdir "$RUNIDRIS_DIR" -i "." -o $FP
16+fi
17+shift
18+"$FP" "$@"
scripts/runidris-nodenew file+18
@@ -0,0 +1,18 @@
1+#!/bin/sh
2+
3+# This is a script that runs an idris program, suitable for use
4+# in a shebang line. We cache the executables by naming them after
5+# the SHA hash of the idris source and looking for it before
6+# compiling. This is the node version.
7+RUNIDRIS_DIR="${TEMP:-/tmp}/runidris-node"
8+if [ ! -d $RUNIDRIS_DIR ]; then
9+ mkdir $RUNIDRIS_DIR
10+ chmod 700 $RUNIDRIS_DIR
11+fi
12+TEMP_NAME="runidris-`sha1sum $1 | cut -c1-40`.js"
13+FP="$RUNIDRIS_DIR/$TEMP_NAME"
14+if [ ! -e $FP ]; then
15+ "${IDRIS:-idris}" --codegen node --ibcsubdir "$RUNIDRIS_DIR" -i "." $1 -o $FP
16+fi
17+shift
18+node "$FP" "$@"
src/IRTS/CodegenC.hs+253−134
@@ -5,9 +5,11 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8+{-# LANGUAGE FlexibleContexts #-}
9+
810module IRTS.CodegenC (codegenC) where
911
10−import Idris.AbsSyntax
12+import Idris.AbsSyntax hiding (getBC)
1113import Idris.Core.TT
1214import IRTS.Bytecode
1315import IRTS.CodegenCommon
@@ -19,10 +21,12 @@ import IRTS.System
1921import Util.System
2022
2123import Control.Monad
24+import Control.Monad
25+import Control.Monad.RWS
2226import Data.Bits
2327import Data.Char
24−import Data.List (intercalate, nubBy)
25−import Debug.Trace
28+import Data.List (find, intercalate, nubBy, partition)
29+import qualified Data.Text as T
2630import Numeric
2731import System.Directory
2832import System.Exit
@@ -30,6 +34,8 @@ import System.FilePath ((<.>), (</>))
3034import System.IO
3135import System.Process
3236
37+import Debug.Trace
38+
3339codegenC :: CodeGenerator
3440codegenC ci = do codegenC' (simpleDecls ci)
3541 (outputFile ci)
@@ -64,7 +70,9 @@ codegenC' defs out exec incs objs libs flags exports iface dbg
6470 let bc = map toBC defs
6571 let wrappers = genWrappers bc
6672 let h = concatMap toDecl (map fst bc)
67− let cc = concatMap (uncurry toC) bc
73+ let (state, cc) = execRWS (generateSrc bc) 0
74+ (CS { fnName = Nothing,
75+ level = 1 })
6876 let hi = concatMap ifaceC (concatMap getExp exports)
6977 d <- getIdrisCRTSDir
7078 mprog <- readFile (d </> "idris_main" <.> "c")
@@ -134,12 +142,17 @@ creg Tmp = "REG1"
134142toDecl :: Name -> String
135143toDecl f = "void " ++ cname f ++ "(VM*, VAL*);\n"
136144
137−toC :: Name -> [BC] -> String
138−toC f code
139− = -- "/* " ++ show code ++ "*/\n\n" ++
140− "void " ++ cname f ++ "(VM* vm, VAL* oldbase) {\n" ++
141− indent 1 ++ "INITFRAME;\n" ++
142− concatMap (bcc 1) code ++ "}\n\n"
145+generateSrc :: [(Name, [BC])] -> RWS Int String CState ()
146+generateSrc bc = mapM_ toC bc
147+
148+toC :: (Name, [BC]) -> RWS Int String CState ()
149+toC (f, code) = do
150+ modify (\s -> s { fnName = Just f })
151+ s <- get
152+ tell $ "void " ++ cname f ++ "(VM* vm, VAL* oldbase) {\n"
153+ tell $ indent (level s) ++ "INITFRAME;\n"
154+ bcc code
155+ tell $ "}\n\n"
143156
144157showCStr :: String -> String
145158showCStr s = '"' : foldr ((++) . showChar) "\"" s
@@ -151,34 +164,46 @@ showCStr s = '"' : foldr ((++) . showChar) "\"" s
151164 -- Note: we need the double quotes around the codes because otherwise
152165 -- "\n3" would get encoded as "\x0a3", which is incorrect.
153166 -- Instead, we opt for "\x0a""3" and let the C compiler deal with it.
154− | ord c < 0x10 = "\"\"\\x0" ++ showHex (ord c) "\"\""
155− | ord c < 0x20 = "\"\"\\x" ++ showHex (ord c) "\"\""
167+ | ord c < 0x20 = showUTF8 (ord c)
156168 | ord c < 0x7f = [c] -- 0x7f = \DEL
157169 | otherwise = showHexes (utf8bytes (ord c))
158170
159− utf8bytes :: Int -> [Int]
160− utf8bytes x = let (h : bytes) = split [] x in
161− headHex h (length bytes) : map toHex bytes
162− where
163− split acc 0 = acc
164− split acc x = let xbits = x .&. 0x3f
165− xrest = shiftR x 6 in
166− split (xbits : acc) xrest
167−
168− headHex h 1 = h + 0xc0
169− headHex h 2 = h + 0xe0
170− headHex h 3 = h + 0xf0
171− headHex h n = error "Can't happen: Invalid UTF8 character"
172−
173− toHex i = i + 0x80
174−
171+ showUTF8 c = "\"\"\\x" ++ pad (showHex c "") ++ "\"\""
175172 showHexes = foldr ((++) . showUTF8) ""
176− showUTF8 c = "\"\"\\x" ++ showHex c "\"\""
177173
178−bcc :: Int -> BC -> String
179−bcc i (ASSIGN l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"
180−bcc i (ASSIGNCONST l c)
181− = indent i ++ creg l ++ " = " ++ mkConst c ++ ";\n"
174+ utf8bytes :: Int -> [Int]
175+ utf8bytes x
176+ | x <= 0x7f = [x]
177+ | x <= 0x7ff = let (y : ys) = split [] 2 x in (y .|. 0xc0) : map (.|. 0x80) ys
178+ | x <= 0xffff = let (y : ys) = split [] 3 x in (y .|. 0xe0) : map (.|. 0x80) ys
179+ | x <= 0x10ffff = let (y : ys) = split [] 4 x in (y .|. 0xf0) : map (.|. 0x80) ys
180+ | otherwise = error $ "Invalid Unicode code point U+" ++ showHex x ""
181+ where
182+ split acc 1 x = x : acc
183+ split acc i x = split (x .&. 0x3f : acc) (i - 1) (shiftR x 6)
184+
185+ pad :: String -> String
186+ pad s = case length s of
187+ 1 -> "0" ++ s
188+ 2 -> s
189+ _ -> error $ "Can't happen: String of invalid length " ++ show s
190+
191+data CState = CS {
192+ fnName :: Maybe Name,
193+ level :: Int
194+}
195+
196+
197+bcc :: [BC] -> RWS Int String CState ()
198+bcc [] = return ()
199+bcc ((ASSIGN l r):xs) = do
200+ i <- get
201+ tell $ indent (level i) ++ creg l ++ " = " ++ creg r ++ ";\n"
202+ bcc xs
203+bcc ((ASSIGNCONST l c):xs) = do
204+ i <- get
205+ tell $ indent (level i) ++ creg l ++ " = " ++ mkConst c ++ ";\n"
206+ bcc xs
182207 where
183208 mkConst (I i) = "MKINT(" ++ show i ++ ")"
184209 mkConst (BI i) | i < (2^30) = "MKINT(" ++ show i ++ ")"
@@ -196,16 +221,21 @@ bcc i (ASSIGNCONST l c)
196221 mkConst c | isTypeConst c = "MKINT(42424242)"
197222 mkConst c = error $ "mkConst of (" ++ show c ++ ") not implemented"
198223
199−bcc i (UPDATE l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"
200−bcc i (MKCON l loc tag []) | tag < 256
201− = indent i ++ creg l ++ " = NULL_CON(" ++ show tag ++ ");\n"
202−bcc i (MKCON l loc tag args)
203− = indent i ++ alloc loc tag ++
204− indent i ++ setArgs 0 args ++ "\n" ++
205− indent i ++ creg l ++ " = " ++ creg Tmp ++ ";\n"
206−
207−-- "MKCON(vm, " ++ creg l ++ ", " ++ show tag ++ ", " ++
208−-- show (length args) ++ concatMap showArg args ++ ");\n"
224+bcc ((UPDATE l r):xs) = do
225+ i <- get
226+ tell $ indent (level i) ++ creg l ++ " = " ++ creg r ++ ";\n"
227+ bcc xs
228+bcc ((MKCON l loc tag []):xs) | tag < 256 = do
229+ i <- get
230+ tell $ indent (level i) ++ creg l ++ " = NULL_CON(" ++ show tag ++ ");\n"
231+ bcc xs
232+bcc ((MKCON l loc tag args):xs) = do
233+ i <- get
234+ let tab = indent (level i)
235+ tell $ tab ++ alloc loc tag ++
236+ tab ++ setArgs 0 args ++ "\n" ++
237+ tab ++ creg l ++ " = " ++ creg Tmp ++ ";\n"
238+ bcc xs
209239 where showArg r = ", " ++ creg r
210240 setArgs i [] = ""
211241 setArgs i (x : xs) = "SETARG(" ++ creg Tmp ++ ", " ++ show i ++ ", " ++ creg x ++
@@ -217,52 +247,94 @@ bcc i (MKCON l loc tag args)
217247 = "updateCon(" ++ creg Tmp ++ ", " ++ creg old ++ ", " ++ show tag ++ ", " ++
218248 show (length args) ++ ");\n"
219249
220−bcc i (PROJECT l loc a) = indent i ++ "PROJECT(vm, " ++ creg l ++ ", " ++ show loc ++
221− ", " ++ show a ++ ");\n"
222−bcc i (PROJECTINTO r t idx)
223− = indent i ++ creg r ++ " = GETARG(" ++ creg t ++ ", " ++ show idx ++ ");\n"
224−bcc i (CASE True r code def)
225− | length code < 4 = showCase i def code
250+bcc ((PROJECT l loc a):xs) = do
251+ i <- get
252+ tell $ indent (level i) ++ "PROJECT(vm, " ++ creg l ++ ", "
253+ ++ show loc ++ ", " ++ show a ++ ");\n"
254+ bcc xs
255+bcc ((PROJECTINTO r t idx):xs) = do
256+ i <- get
257+ tell $ indent (level i) ++ creg r ++ " = GETARG(" ++ creg t
258+ ++ ", " ++ show idx ++ ");\n"
259+ bcc xs
260+bcc ((CASE True r code def):xs)
261+ | length code < 4 = do
262+ showCases def code
263+ bcc xs
226264 where
227− showCode :: Int -> [BC] -> String
228− showCode i bc = "{\n" ++ concatMap (bcc (i + 1)) bc ++
229− indent i ++ "}\n"
230−
231− showCase :: Int -> Maybe [BC] -> [(Int, [BC])] -> String
232− showCase i Nothing [(t, c)] = indent i ++ showCode i c
233− showCase i (Just def) [] = indent i ++ showCode i def
234− showCase i def ((t, c) : cs)
235− = indent i ++ "if (CTAG(" ++ creg r ++ ") == " ++ show t ++ ") " ++ showCode i c
236− ++ indent i ++ "else\n" ++ showCase i def cs
237−
238−bcc i (CASE safe r code def)
239− = indent i ++ "switch(" ++ ctag safe ++ "(" ++ creg r ++ ")) {\n" ++
240− concatMap (showCase i) code ++
241− showDef i def ++
242− indent i ++ "}\n"
265+ showCode bc = do
266+ w <- getBC bc xs
267+ i <- get
268+ tell $ "{\n" ++ w ++ indent (level i) ++ "}\n"
269+
270+ showCases Nothing [(t, c)] = do
271+ i <- get
272+ tell $ indent (level i)
273+ showCode c
274+ showCases (Just def) [] = do
275+ i <- get
276+ tell $ indent (level i)
277+ showCode def
278+ showCases def ((t, c) : cs) = do
279+ i <- get
280+ tell $ indent (level i) ++ "if (CTAG(" ++ creg r ++ ") == "
281+ ++ show t ++ ") "
282+ showCode c
283+ tell $ indent (level i) ++ "else\n"
284+ showCases def cs
285+
286+bcc ((CASE safe r code def):xs) = do
287+ i <- get
288+ tell $ indent (level i) ++ "switch(" ++ ctag safe ++ "(" ++ creg r ++ ")) {\n"
289+ mapM showCase code
290+ showDef def
291+ tell $ indent (level i) ++ "}\n"
292+ bcc xs
243293 where
244294 ctag True = "CTAG"
245295 ctag False = "TAG"
246296
247− showCase i (t, bc) = indent i ++ "case " ++ show t ++ ":\n"
248− ++ concatMap (bcc (i+1)) bc ++ indent (i + 1) ++ "break;\n"
249− showDef i Nothing = ""
250− showDef i (Just c) = indent i ++ "default:\n"
251− ++ concatMap (bcc (i+1)) c ++ indent (i + 1) ++ "break;\n"
252−bcc i (CONSTCASE r code def)
297+ showCase (t, bc) = do
298+ w <- getBC bc xs
299+ is <- get
300+ let i = level is
301+ tell $ indent i ++ "case " ++ show t ++ ":\n"
302+ ++ w ++ indent (i + 1) ++ "break;\n"
303+ showDef Nothing = return $ ()
304+ showDef (Just c) = do
305+ w <- getBC c xs
306+ is <- get
307+ let i = level is
308+ tell $ indent i ++ "default:\n" ++ w ++ indent (i + 1) ++ "break;\n"
309+
310+bcc ((CONSTCASE r code def):xs)
253311 | intConsts code
254−-- = indent i ++ "switch(GETINT(" ++ creg r ++ ")) {\n" ++
255−-- concatMap (showCase i) code ++
256−-- showDef i def ++
257−-- indent i ++ "}\n"
258− = concatMap (iCase (creg r)) code ++
259− indent i ++ "{\n" ++ showDefS i def ++ indent i ++ "}\n"
312+ = do
313+ is <- get
314+ let i = level is
315+ codes <- mapM getCode code
316+ defs <- showDefS def
317+ tell $ concatMap (iCase i (creg r)) codes
318+ tell $ indent i ++ "{\n" ++ defs ++ indent i ++ "}\n"
319+ bcc xs
260320 | strConsts code
261− = concatMap (strCase ("GETSTR(" ++ creg r ++ ")")) code ++
262− indent i ++ "{\n" ++ showDefS i def ++ indent i ++ "}\n"
321+ = do
322+ is <- get
323+ let i = level is
324+ codes <- mapM getCode code
325+ defs <- showDefS def
326+ tell $ concatMap (strCase i ("GETSTR(" ++ creg r ++ ")")) codes
327+ ++ indent i ++ "{\n" ++ defs ++ indent i ++ "}\n"
328+ bcc xs
263329 | bigintConsts code
264− = concatMap (biCase (creg r)) code ++
265− indent i ++ "{\n" ++ showDefS i def ++ indent i ++ "}\n"
330+ = do
331+ is <- get
332+ let i = level is
333+ codes <- mapM getCode code
334+ defs <- showDefS def
335+ tell $ concatMap (biCase i (creg r)) codes ++
336+ indent i ++ "{\n" ++ defs ++ indent i ++ "}\n"
337+ bcc xs
266338 | otherwise = error $ "Can't happen: Can't compile const case " ++ show code
267339 where
268340 intConsts ((I _, _ ) : _) = True
@@ -279,72 +351,119 @@ bcc i (CONSTCASE r code def)
279351 strConsts ((Str _, _ ) : _) = True
280352 strConsts _ = False
281353
282− strCase sv (s, bc) =
354+ getCode (x, code) = do
355+ c <- getBC code xs
356+ return (x, c)
357+
358+ strCase i sv (s, bc) =
283359 indent i ++ "if (strcmp(" ++ sv ++ ", " ++ show s ++ ") == 0) {\n" ++
284− concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
285− biCase bv (BI b, bc) =
360+ bc ++ indent i ++ "} else\n"
361+ biCase i bv (BI b, bc) =
286362 indent i ++ "if (bigEqConst(" ++ bv ++ ", " ++ show b ++ ")) {\n"
287− ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
288− iCase v (I b, bc) =
363+ ++ bc ++ indent i ++ "} else\n"
364+ iCase i v (I b, bc) =
289365 indent i ++ "if (GETINT(" ++ v ++ ") == " ++ show b ++ ") {\n"
290− ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
291− iCase v (Ch b, bc) =
366+ ++ bc ++ indent i ++ "} else\n"
367+ iCase i v (Ch b, bc) =
292368 indent i ++ "if (GETINT(" ++ v ++ ") == " ++ show (fromEnum b) ++ ") {\n"
293− ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
294− iCase v (B8 w, bc) =
369+ ++ bc ++ indent i ++ "} else\n"
370+ iCase i v (B8 w, bc) =
295371 indent i ++ "if (GETBITS8(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"
296− ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
297− iCase v (B16 w, bc) =
372+ ++ bc ++ indent i ++ "} else\n"
373+ iCase i v (B16 w, bc) =
298374 indent i ++ "if (GETBITS16(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"
299− ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
300− iCase v (B32 w, bc) =
375+ ++ bc ++ indent i ++ "} else\n"
376+ iCase i v (B32 w, bc) =
301377 indent i ++ "if (GETBITS32(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"
302− ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
303− iCase v (B64 w, bc) =
378+ ++ bc ++ indent i ++ "} else\n"
379+ iCase i v (B64 w, bc) =
304380 indent i ++ "if (GETBITS64(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"
305− ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
306− showCase i (t, bc) = indent i ++ "case " ++ show t ++ ":\n"
307− ++ concatMap (bcc (i+1)) bc ++
308− indent (i + 1) ++ "break;\n"
309− showDef i Nothing = ""
310− showDef i (Just c) = indent i ++ "default:\n"
311− ++ concatMap (bcc (i+1)) c ++
312− indent (i + 1) ++ "break;\n"
313− showDefS i Nothing = ""
314− showDefS i (Just c) = concatMap (bcc (i+1)) c
315−
316−bcc i (CALL n) = indent i ++ "CALL(" ++ cname n ++ ");\n"
317−bcc i (TAILCALL n) = indent i ++ "TAILCALL(" ++ cname n ++ ");\n"
318−bcc i (SLIDE n) = indent i ++ "SLIDE(vm, " ++ show n ++ ");\n"
319−bcc i REBASE = indent i ++ "REBASE;\n"
320−bcc i (RESERVE 0) = ""
321−bcc i (RESERVE n) = indent i ++ "RESERVE(" ++ show n ++ ");\n"
322−bcc i (ADDTOP 0) = ""
323−bcc i (ADDTOP n) = indent i ++ "ADDTOP(" ++ show n ++ ");\n"
324−bcc i (TOPBASE n) = indent i ++ "TOPBASE(" ++ show n ++ ");\n"
325−bcc i (BASETOP n) = indent i ++ "BASETOP(" ++ show n ++ ");\n"
326−bcc i STOREOLD = indent i ++ "STOREOLD;\n"
327−bcc i (OP l fn args) = indent i ++ doOp (creg l ++ " = ") fn args ++ ";\n"
328−bcc i (FOREIGNCALL l rty (FStr fn@('&':name)) [])
329− = indent i ++
330− c_irts (toFType rty) (creg l ++ " = ") fn ++ ";\n"
331−bcc i (FOREIGNCALL l rty (FStr fn) (x:xs)) | fn == "%wrapper"
332− = indent i ++
333− c_irts (toFType rty) (creg l ++ " = ")
381+ ++ bc ++ indent i ++ "} else\n"
382+
383+ showDefS Nothing = return ""
384+ showDefS (Just c) = getBC c xs
385+
386+bcc (CALL n:xs) = do
387+ i <- get
388+ tell $ indent (level i) ++ "CALL(" ++ cname n ++ ");\n"
389+ bcc xs
390+bcc (TAILCALL n:xs) = do
391+ i <- get
392+ tell $ indent (level i) ++ "TAILCALL(" ++ cname n ++ ");\n"
393+ bcc xs
394+bcc ((SLIDE n):xs) = do
395+ i <- get
396+ tell $ indent (level i) ++ "SLIDE(vm, " ++ show n ++ ");\n"
397+ bcc xs
398+bcc (REBASE:xs) = do
399+ i <- get
400+ tell $ indent (level i)++ "REBASE;\n"
401+ bcc xs
402+bcc ((RESERVE 0):xs) = bcc xs
403+bcc ((RESERVE n):xs) = do
404+ i <- get
405+ tell $ indent (level i) ++ "RESERVE(" ++ show n ++ ");\n"
406+ bcc xs
407+bcc ((ADDTOP 0):xs) = bcc xs
408+bcc ((ADDTOP n):xs) = do
409+ i <- get
410+ tell $ indent (level i) ++ "ADDTOP(" ++ show n ++ ");\n"
411+ bcc xs
412+bcc ((TOPBASE n):xs) = do
413+ i <- get
414+ tell $ indent (level i) ++ "TOPBASE(" ++ show n ++ ");\n"
415+ bcc xs
416+bcc ((BASETOP n):xs) = do
417+ i <- get
418+ tell $ indent (level i) ++ "BASETOP(" ++ show n ++ ");\n"
419+ bcc xs
420+bcc (STOREOLD:xs) = do
421+ i <- get
422+ tell $ indent (level i) ++ "STOREOLD;\n"
423+ bcc xs
424+bcc ((OP l fn args):xs) = do
425+ i <- get
426+ tell $ indent (level i) ++ doOp (creg l ++ " = ") fn args ++ ";\n"
427+ bcc xs
428+bcc ((FOREIGNCALL l rty (FStr fn@('&':name)) []):xs) = do
429+ i <- get
430+ tell $ indent (level i) ++ c_irts (toFType rty) (creg l ++ " = ") fn ++ ";\n"
431+ bcc xs
432+bcc ((FOREIGNCALL l rty (FStr fn) (x:xs)):zs) | fn == "%wrapper"
433+ = do
434+ i <- get
435+ tell $ indent (level i) ++ c_irts (toFType rty) (creg l ++ " = ")
334436 ("_idris_get_wrapper(" ++ creg (snd x) ++ ")") ++ ";\n"
335−bcc i (FOREIGNCALL l rty (FStr fn) (x:xs)) | fn == "%dynamic"
336− = indent i ++ c_irts (toFType rty) (creg l ++ " = ")
437+ bcc zs
438+bcc ((FOREIGNCALL l rty (FStr fn) (x:xs)):zs) | fn == "%dynamic"
439+ = do
440+ i <- get
441+ tell $ indent (level i) ++ c_irts (toFType rty) (creg l ++ " = ")
337442 ("(*(" ++ cFnSig "" rty xs ++ ") GETPTR(" ++ creg (snd x) ++ "))" ++
338443 "(" ++ showSep "," (map fcall xs) ++ ")") ++ ";\n"
339−bcc i (FOREIGNCALL l rty (FStr fn) args)
340− = indent i ++
341− c_irts (toFType rty) (creg l ++ " = ")
342− (fn ++ "(" ++ showSep "," (map fcall args) ++ ")") ++ ";\n"
343−bcc i (FOREIGNCALL l rty _ args) = error "Foreign Function calls cannot be partially applied, without being inlined."
344−bcc i (NULL r) = indent i ++ creg r ++ " = NULL;\n" -- clear, so it'll be GCed
345−bcc i (ERROR str) = indent i ++ "fprintf(stderr, " ++ show str ++ "); fprintf(stderr, \"\\n\"); exit(-1);\n"
444+ bcc zs
445+bcc ((FOREIGNCALL l rty (FStr fn) args):xs) = do
446+ i <- get
447+ tell $ indent (level i) ++ c_irts (toFType rty) (creg l ++ " = ")
448+ (fn ++ "(" ++ showSep "," (map fcall args) ++ ")") ++ ";\n"
449+ bcc xs
450+bcc ((FOREIGNCALL l rty _ args):_) = error "Foreign Function calls cannot be partially applied, without being inlined."
451+bcc ((NULL r):xs) = do
452+ i <- get
453+ tell $ indent (level i) ++ creg r ++ " = NULL;\n" -- clear, so it'll be GCed
454+ bcc xs
455+bcc ((ERROR str):xs) = do
456+ i <- get
457+ tell $ indent (level i) ++ "fprintf(stderr, "
458+ ++ show str ++ "); fprintf(stderr, \"\\n\"); exit(-1);\n"
459+ bcc xs
346460-- bcc i c = error (show c) -- indent i ++ "// not done yet\n"
347461
462+getBC code xs = do
463+ i <- get
464+ let (a, s, w) = runRWS (bcc code) 0 (i { level = level i + 1 })
465+ return w
466+
348467fcall (t, arg) = irts_c (toFType t) (creg arg)
349468-- Deconstruct the Foreign type in the defunctionalised expression and build
350469-- a foreign type description for c_irts and irts_c
src/IRTS/Compiler.hs+2−1
@@ -5,7 +5,7 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8−{-# LANGUAGE CPP, PatternGuards, TypeSynonymInstances #-}
8+{-# LANGUAGE CPP, FlexibleContexts, PatternGuards, TypeSynonymInstances #-}
99
1010module IRTS.Compiler(compile, generate) where
1111
@@ -17,6 +17,7 @@ import Idris.Core.Evaluate
1717import Idris.Core.TT
1818import Idris.Erasure
1919import Idris.Error
20+import Idris.Options
2021import Idris.Output
2122import IRTS.CodegenC
2223import IRTS.CodegenCommon
src/IRTS/Defunctionalise.hs+1−1
@@ -19,7 +19,7 @@ To defunctionalise:
19198. Add explicit EVAL to case, primitives, and foreign calls
2020
2121-}
22−{-# LANGUAGE PatternGuards #-}
22+{-# LANGUAGE FlexibleContexts, PatternGuards #-}
2323module IRTS.Defunctionalise(module IRTS.Defunctionalise
2424 , module IRTS.Lang
2525 ) where
src/IRTS/JavaScript/AST.hs+8−19
@@ -99,35 +99,24 @@ data JsExpr
9999
100100translateChar :: Char -> String
101101translateChar ch
102− | '\a' <- ch = "\\u0007"
103102 | '\b' <- ch = "\\b"
104103 | '\f' <- ch = "\\f"
105104 | '\n' <- ch = "\\n"
106105 | '\r' <- ch = "\\r"
107106 | '\t' <- ch = "\\t"
108107 | '\v' <- ch = "\\v"
109− | '\SO' <- ch = "\\u000E"
110− | '\DEL' <- ch = "\\u007F"
111108 | '\\' <- ch = "\\\\"
112109 | '\"' <- ch = "\\\""
113110 | '\'' <- ch = "\\\'"
114− | ch `elem` asciiTab = "\\u" ++ fill (showHex (ord ch) "")
115− | ord ch > 255 = "\\u" ++ fill (showHex (ord ch) "")
116− | otherwise = [ch]
111+ | ord ch < 0x20 = "\\x" ++ pad 2 (showHex (ord ch) "")
112+ | ord ch < 0x7f = [ch] -- 0x7f '\DEL'
113+ | ord ch <= 0xff = "\\x" ++ pad 2 (showHex (ord ch) "")
114+ | ord ch <= 0xffff = "\\u" ++ pad 4 (showHex (ord ch) "")
115+ | ord ch <= 0x10ffff = "\\u{" ++ showHex (ord ch) "}"
116+ | otherwise = error $ "Invalid Unicode code point U+" ++ showHex (ord ch) ""
117117 where
118− fill :: String -> String
119− fill s = case length s of
120− 1 -> "000" ++ s
121− 2 -> "00" ++ s
122− 3 -> "0" ++ s
123− _ -> s
124−
125− asciiTab =
126− ['\NUL', '\SOH', '\STX', '\ETX', '\EOT', '\ENQ', '\ACK', '\BEL',
127− '\BS', '\HT', '\LF', '\VT', '\FF', '\CR', '\SO', '\SI',
128− '\DLE', '\DC1', '\DC2', '\DC3', '\DC4', '\NAK', '\SYN', '\ETB',
129− '\CAN', '\EM', '\SUB', '\ESC', '\FS', '\GS', '\RS', '\US']
130−
118+ pad :: Int -> String -> String
119+ pad n s = replicate (n - length s) '0' ++ s
131120
132121indent :: Text -> Text
133122indent x =
src/IRTS/JavaScript/Codegen.hs+11−2
@@ -64,7 +64,14 @@ data CGConf = CGConf { header :: Text
6464
6565
6666getInclude :: FilePath -> IO Text
67−getInclude p = TIO.readFile p
67+getInclude p =
68+ do
69+ libs <- getIdrisLibDir
70+ let libPath = libs </> p
71+ exitsInLib <- doesFileExist libPath
72+ if exitsInLib then
73+ TIO.readFile libPath
74+ else TIO.readFile p
6875
6976getIncludes :: [FilePath] -> IO Text
7077getIncludes l = do
@@ -76,6 +83,7 @@ includeLibs =
7683 let
7784 repl '\\' = '_'
7885 repl '/' = '_'
86+ repl '.' = '_'
7987 repl c = c
8088 in
8189 concatMap (\lib -> "var " ++ (repl <$> lib) ++ " = require(\"" ++ lib ++"\");\n")
@@ -90,7 +98,8 @@ codegenJs :: CGConf -> CodeGenerator
9098codegenJs conf ci =
9199 do
92100 debug <- isYes <$> lookupEnv "IDRISJS_DEBUG"
93− let defs = Map.fromList $ liftDecls ci
101+ let defs' = Map.fromList $ liftDecls ci
102+ let defs = globlToCon defs'
94103 let used = Map.elems $ removeDeadCode defs [sMN 0 "runMain"]
95104 if debug then
96105 do
src/IRTS/JavaScript/LangTransforms.hs+13
@@ -8,6 +8,7 @@ Maintainer : The Idris Community.
88{-# LANGUAGE DeriveDataTypeable, OverloadedStrings, StandaloneDeriving #-}
99
1010module IRTS.JavaScript.LangTransforms( removeDeadCode
11+ , globlToCon
1112 ) where
1213
1314
@@ -94,3 +95,15 @@ removeDeadCode dcls start =
9495 remCons = removeUnusedBranches (getUsedConstructors used) used
9596 in if Map.keys remCons == Map.keys dcls then remCons
9697 else removeDeadCode remCons start
98+
99+
100+globlToCon :: Map Name LDecl -> Map Name LDecl
101+globlToCon x =
102+ transformBi (f x) x
103+ where
104+ f :: Map Name LDecl -> LExp -> LExp
105+ f y x@(LV (Glob n)) =
106+ case Map.lookup n y of
107+ Just (LConstructor _ conId arity) -> LCon Nothing conId n []
108+ _ -> x
109+ f y x = x
src/IRTS/JavaScript/PrimOp.hs+11−3
@@ -28,7 +28,7 @@ import IRTS.Lang
2828data JsPrimTy = PTBool | PTAny deriving (Eq, Ord)
2929
3030type PrimF = [JsExpr] -> JsExpr
31−type PrimDec = (Bool, JsPrimTy, PrimF)
31+type PrimDec = (Bool, JsPrimTy, PrimF) -- the bool indicates if bigint library is used or not
3232
3333deriving instance Ord PrimFn
3434
@@ -177,15 +177,22 @@ primDB =
177177 , item (LZExt (ITFixed IT16) ITNative) False PTAny $ head
178178 , item (LZExt (ITFixed IT32) ITNative) False PTAny $ head
179179 , item (LZExt ITNative ITBig) True PTAny $ JsForeign "new $JSRTS.jsbn.BigInteger(''+%0)"
180+ , item (LZExt (ITFixed IT8) ITBig) True PTAny $ JsForeign "new $JSRTS.jsbn.BigInteger(''+%0)"
181+ , item (LZExt (ITFixed IT16) ITBig) True PTAny $ JsForeign "new $JSRTS.jsbn.BigInteger(''+%0)"
182+ , item (LZExt (ITFixed IT32) ITBig) True PTAny $ JsForeign "new $JSRTS.jsbn.BigInteger(''+%0)"
183+ , item (LZExt (ITFixed IT64) ITBig) True PTAny $ head
180184 , item (LTrunc ITBig ITNative) True PTAny $ JsForeign "%0.intValue()|0"
185+ , item (LTrunc ITBig (ITFixed IT8)) True PTAny $ JsForeign "%0.intValue() & 0xFF"
186+ , item (LTrunc ITBig (ITFixed IT16)) True PTAny $ JsForeign "%0.intValue() & 0xFFFF"
187+ , item (LTrunc ITBig (ITFixed IT32)) True PTAny $ JsForeign "%0.intValue() & 0xFFFFFFFF"
188+ , item (LTrunc ITBig (ITFixed IT64)) True PTAny $
189+ \[x] -> JsForeign "%0.and(new $JSRTS.jsbn.BigInteger(%1))" [x, JsStr $ show 0xFFFFFFFFFFFFFFFF]
181190 , item (LTrunc (ITFixed IT16) (ITFixed IT8)) False PTAny $ JsForeign "%0 & 0xFF"
182191 , item (LTrunc (ITFixed IT32) (ITFixed IT8)) False PTAny $ JsForeign "%0 & 0xFF"
183192 , item (LTrunc (ITFixed IT64) (ITFixed IT8)) True PTAny $ JsForeign "%0.intValue() & 0xFF"
184193 , item (LTrunc (ITFixed IT32) (ITFixed IT16)) False PTAny $ JsForeign "%0 & 0xFFFF"
185194 , item (LTrunc (ITFixed IT64) (ITFixed IT16)) True PTAny $ JsForeign "%0.intValue() & 0xFFFF"
186195 , item (LTrunc (ITFixed IT64) (ITFixed IT32)) True PTAny $ JsForeign "%0.intValue() & 0xFFFFFFFF"
187− , item (LTrunc ITBig (ITFixed IT64)) True PTAny $
188− \[x] -> JsForeign "%0.and(new $JSRTS.jsbn.BigInteger(%1))" [x, JsStr $ show 0xFFFFFFFFFFFFFFFF]
189196 , item LStrConcat False PTAny $ binop "+"
190197 , item LStrLt False PTBool $ binop "<"
191198 , item LStrEq False PTBool $ binop "=="
@@ -193,6 +200,7 @@ primDB =
193200 , item (LIntFloat ITNative) False PTAny $ head
194201 , item (LIntFloat ITBig) True PTAny $ JsForeign "%0.intValue()"
195202 , item (LFloatInt ITNative) False PTAny $ JsForeign "%0|0"
203+ , item (LFloatInt ITBig) True PTAny $ JsForeign "new $JSRTS.jsbn.BigInteger(Math.trunc(%0)+ '')"
196204 , item (LIntStr ITNative) False PTAny $ JsForeign "''+%0"
197205 , item (LIntStr ITBig) True PTAny $ JsForeign "%0.toString()"
198206 , item (LStrInt ITNative) False PTAny $ JsForeign "parseInt(%0)|0"
src/IRTS/Lang.hs+2−1
@@ -5,7 +5,8 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8−{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveGeneric, PatternGuards #-}
8+{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveGeneric, FlexibleContexts,
9+ PatternGuards #-}
910
1011module IRTS.Lang where
1112
src/IRTS/Portable.hs+1−1
@@ -5,7 +5,7 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8−{-# LANGUAGE OverloadedStrings #-}
8+{-# LANGUAGE FlexibleInstances, OverloadedStrings, TypeSynonymInstances #-}
99module IRTS.Portable (writePortable) where
1010
1111import Idris.Core.CaseTree
src/IRTS/Simplified.hs+1
@@ -5,6 +5,7 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8+{-# LANGUAGE FlexibleContexts #-}
89module IRTS.Simplified(simplifyDefs, SDecl(..), SExp(..), SAlt(..)) where
910
1011import Idris.Core.CaseTree
src/Idris/ASTUtils.hs+1
@@ -48,6 +48,7 @@ module Idris.ASTUtils(
4848import Idris.AbsSyntaxTree
4949import Idris.Core.Evaluate
5050import Idris.Core.TT
51+import Idris.Options
5152
5253import Prelude hiding (id, (.))
5354
src/Idris/AbsSyntax.hs+3−124
@@ -6,7 +6,7 @@ License : BSD3
66Maintainer : The Idris Community.
77-}
88
9−{-# LANGUAGE DeriveFunctor, PatternGuards #-}
9+{-# LANGUAGE DeriveFunctor, FlexibleContexts, PatternGuards #-}
1010
1111module Idris.AbsSyntax(
1212 module Idris.AbsSyntax
@@ -19,6 +19,7 @@ import Idris.Core.Evaluate
1919import Idris.Core.TT
2020import Idris.Docstrings
2121import Idris.IdeMode hiding (Opt(..))
22+import Idris.Options
2223import IRTS.CodegenCommon
2324
2425import System.Directory (canonicalizePath, doesFileExist)
@@ -2602,126 +2603,4 @@ mkUniqueNames env shadows tm
26022603
26032604 mkUniq ql nmap tm = descendM (mkUniq ql nmap) tm
26042605
2605−getFile :: Opt -> Maybe String
2606−getFile (Filename s) = Just s
2607−getFile _ = Nothing
2608−
2609−getBC :: Opt -> Maybe String
2610−getBC (BCAsm s) = Just s
2611−getBC _ = Nothing
2612−
2613−getOutput :: Opt -> Maybe String
2614−getOutput (Output s) = Just s
2615−getOutput _ = Nothing
2616−
2617−getIBCSubDir :: Opt -> Maybe String
2618−getIBCSubDir (IBCSubDir s) = Just s
2619−getIBCSubDir _ = Nothing
2620−
2621−getImportDir :: Opt -> Maybe String
2622−getImportDir (ImportDir s) = Just s
2623−getImportDir _ = Nothing
2624−
2625−getSourceDir :: Opt -> Maybe String
2626−getSourceDir (SourceDir s) = Just s
2627−getSourceDir _ = Nothing
2628−
2629−getPkgDir :: Opt -> Maybe String
2630−getPkgDir (Pkg s) = Just s
2631−getPkgDir _ = Nothing
2632−
2633−getPkg :: Opt -> Maybe (Bool, String)
2634−getPkg (PkgBuild s) = Just (False, s)
2635−getPkg (PkgInstall s) = Just (True, s)
2636−getPkg _ = Nothing
2637−
2638−getPkgClean :: Opt -> Maybe String
2639−getPkgClean (PkgClean s) = Just s
2640−getPkgClean _ = Nothing
2641−
2642−getPkgREPL :: Opt -> Maybe String
2643−getPkgREPL (PkgREPL s) = Just s
2644−getPkgREPL _ = Nothing
2645−
2646−getPkgCheck :: Opt -> Maybe String
2647−getPkgCheck (PkgCheck s) = Just s
2648−getPkgCheck _ = Nothing
2649−
2650−-- | Returns None if given an Opt which is not PkgMkDoc
2651−-- Otherwise returns Just x, where x is the contents of PkgMkDoc
2652−getPkgMkDoc :: Opt -- ^ Opt to extract
2653− -> Maybe (Bool, String) -- ^ Result
2654−getPkgMkDoc (PkgDocBuild str) = Just (False,str)
2655−getPkgMkDoc (PkgDocInstall str) = Just (True,str)
2656−getPkgMkDoc _ = Nothing
2657−
2658−getPkgTest :: Opt -- ^ the option to extract
2659− -> Maybe String -- ^ the package file to test
2660−getPkgTest (PkgTest f) = Just f
2661−getPkgTest _ = Nothing
2662−
2663−getCodegen :: Opt -> Maybe Codegen
2664−getCodegen (UseCodegen x) = Just x
2665−getCodegen _ = Nothing
2666−
2667−getCodegenArgs :: Opt -> Maybe String
2668−getCodegenArgs (CodegenArgs args) = Just args
2669−getCodegenArgs _ = Nothing
2670−
2671−getConsoleWidth :: Opt -> Maybe ConsoleWidth
2672−getConsoleWidth (UseConsoleWidth x) = Just x
2673−getConsoleWidth _ = Nothing
2674−
2675−getExecScript :: Opt -> Maybe String
2676−getExecScript (InterpretScript expr) = Just expr
2677−getExecScript _ = Nothing
2678−
2679−getPkgIndex :: Opt -> Maybe FilePath
2680−getPkgIndex (PkgIndex file) = Just file
2681−getPkgIndex _ = Nothing
2682−
2683−getEvalExpr :: Opt -> Maybe String
2684−getEvalExpr (EvalExpr expr) = Just expr
2685−getEvalExpr _ = Nothing
2686−
2687−getOutputTy :: Opt -> Maybe OutputType
2688−getOutputTy (OutputTy t) = Just t
2689−getOutputTy _ = Nothing
2690−
2691−getLanguageExt :: Opt -> Maybe LanguageExt
2692−getLanguageExt (Extension e) = Just e
2693−getLanguageExt _ = Nothing
2694−
2695−getTriple :: Opt -> Maybe String
2696−getTriple (TargetTriple x) = Just x
2697−getTriple _ = Nothing
2698−
2699−getCPU :: Opt -> Maybe String
2700−getCPU (TargetCPU x) = Just x
2701−getCPU _ = Nothing
2702−
2703−getOptLevel :: Opt -> Maybe Int
2704−getOptLevel (OptLevel x) = Just x
2705−getOptLevel _ = Nothing
2706−
2707−getOptimisation :: Opt -> Maybe (Bool,Optimisation)
2708−getOptimisation (AddOpt p) = Just (True, p)
2709−getOptimisation (RemoveOpt p) = Just (False, p)
2710−getOptimisation _ = Nothing
2711−
2712−getColour :: Opt -> Maybe Bool
2713−getColour (ColourREPL b) = Just b
2714−getColour _ = Nothing
2715−
2716−getClient :: Opt -> Maybe String
2717−getClient (Client x) = Just x
2718−getClient _ = Nothing
2719−
2720−-- Get the first valid port
2721−getPort :: [Opt] -> Maybe REPLPort
2722−getPort [] = Nothing
2723−getPort (Port p : _ ) = Just p
2724−getPort (_ : xs) = getPort xs
2725−
2726−opt :: (Opt -> Maybe a) -> [Opt] -> [a]
2727−opt = mapMaybe
2606+
src/Idris/AbsSyntaxTree.hs+13−134
@@ -6,7 +6,9 @@ License : BSD3
66Maintainer : The Idris Community.
77-}
88
9−{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveGeneric, PatternGuards #-}
9+{-# LANGUAGE DeriveDataTypeable, DeriveFoldable, DeriveFunctor, DeriveGeneric,
10+ DeriveTraversable, FlexibleContexts, FlexibleInstances,
11+ MultiParamTypeClasses, PatternGuards, TypeSynonymInstances #-}
1012
1113module Idris.AbsSyntaxTree where
1214
@@ -14,6 +16,7 @@ import Idris.Core.Elaborate hiding (Tactic(..))
1416import Idris.Core.Evaluate
1517import Idris.Core.TT
1618import Idris.Docstrings
19+import Idris.Options
1720import IRTS.CodegenCommon
1821import IRTS.Lang
1922import Util.DynamicLinker
@@ -146,8 +149,7 @@ data PPOption = PPOption {
146149 , ppopt_depth :: Maybe Int
147150 } deriving (Show)
148151
149−data Optimisation = PETransform -- ^ partial eval and associated transforms
150− deriving (Show, Eq, Generic)
152+
151153
152154defaultOptimise :: [Optimisation]
153155defaultOptimise = []
@@ -183,21 +185,12 @@ ppOption opt = PPOption {
183185ppOptionIst :: IState -> PPOption
184186ppOptionIst = ppOption . idris_options
185187
186−data LanguageExt = TypeProviders | ErrorReflection | UniquenessTypes
187− | DSLNotation | ElabReflection | FCReflection
188− | LinearTypes
189− deriving (Show, Eq, Read, Ord, Generic)
190188
191189-- | The output mode in use
192190data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle
193191 | IdeMode Integer Handle -- ^ Send IDE output for some request ID to the handle
194192 deriving Show
195193
196−-- | How wide is the console?
197−data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken
198− | ColsWide Int -- ^ Manually specified - must be positive
199− | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise
200− deriving (Show, Eq, Generic)
201194
202195-- | If a function has no totality annotation, what do we assume?
203196data DefaultTotality = DefaultCheckingTotal -- ^ Total
@@ -434,53 +427,7 @@ throwError = Trans.lift . throwE
434427
435428-- Commands in the REPL
436429
437−data Codegen = Via IRFormat String
438− | Bytecode
439− deriving (Show, Eq, Generic)
440−
441−data IRFormat = IBCFormat | JSONFormat deriving (Show, Eq, Generic)
442−
443−data HowMuchDocs = FullDocs | OverviewDocs
444430
445−data OutputFmt = HTMLOutput | LaTeXOutput
446−
447−-- | Recognised logging categories for the Idris compiler.
448−--
449−-- @TODO add in sub categories.
450−data LogCat = IParse
451− | IElab
452− | ICodeGen
453− | IErasure
454− | ICoverage
455− | IIBC
456− deriving (Show, Eq, Ord, Generic)
457−
458−strLogCat :: LogCat -> String
459−strLogCat IParse = "parser"
460−strLogCat IElab = "elab"
461−strLogCat ICodeGen = "codegen"
462−strLogCat IErasure = "erasure"
463−strLogCat ICoverage = "coverage"
464−strLogCat IIBC = "ibc"
465−
466−codegenCats :: [LogCat]
467−codegenCats = [ICodeGen]
468−
469−parserCats :: [LogCat]
470−parserCats = [IParse]
471−
472−elabCats :: [LogCat]
473−elabCats = [IElab]
474−
475−loggingCatsStr :: String
476−loggingCatsStr = unlines
477− [ (strLogCat IParse)
478− , (strLogCat IElab)
479− , (strLogCat ICodeGen)
480− , (strLogCat IErasure)
481− , (strLogCat ICoverage)
482− , (strLogCat IIBC)
483− ]
484431
485432
486433data ElabShellCmd = EQED
@@ -494,83 +441,8 @@ data ElabShellCmd = EQED
494441 | EDocStr (Either Name Const)
495442 deriving (Show, Eq)
496443
497−data Opt = Filename String
498− | Quiet
499− | NoBanner
500− | ColourREPL Bool
501− | Idemode
502− | IdemodeSocket
503− | IndentWith Int
504− | IndentClause Int
505− | ShowAll
506− | ShowLibs
507− | ShowLibDir
508− | ShowDocDir
509− | ShowIncs
510− | ShowPkgs
511− | ShowLoggingCats
512− | NoBasePkgs
513− | NoPrelude
514− | NoBuiltins -- only for the really primitive stuff!
515− | NoREPL
516− | OLogging Int
517− | OLogCats [LogCat]
518− | Output String
519− | Interface
520− | TypeCase
521− | TypeInType
522− | DefaultTotal
523− | DefaultPartial
524− | WarnPartial
525− | WarnReach
526− | AuditIPkg
527− | EvalTypes
528− | NoCoverage
529− | ErrContext
530− | ShowImpl
531− | Verbose Int
532− | Port REPLPort -- ^ REPL TCP port
533− | IBCSubDir String
534− | ImportDir String
535− | SourceDir String
536− | PkgBuild String
537− | PkgInstall String
538− | PkgClean String
539− | PkgCheck String
540− | PkgREPL String
541− | PkgDocBuild String -- IdrisDoc
542− | PkgDocInstall String
543− | PkgTest String
544− | PkgIndex FilePath
545− | WarnOnly
546− | Pkg String
547− | BCAsm String
548− | DumpDefun String
549− | DumpCases String
550− | UseCodegen Codegen
551− | CodegenArgs String
552− | OutputTy OutputType
553− | Extension LanguageExt
554− | InterpretScript String
555− | EvalExpr String
556− | TargetTriple String
557− | TargetCPU String
558− | OptLevel Int
559− | AddOpt Optimisation
560− | RemoveOpt Optimisation
561− | Client String
562− | ShowOrigErr
563− | AutoWidth -- ^ Automatically adjust terminal width
564− | AutoSolve -- ^ Automatically issue "solve" tactic in old-style interactive prover
565− | UseConsoleWidth ConsoleWidth
566− | DumpHighlights
567− | DesugarNats
568− | NoElimDeprecationWarnings -- ^ Don't show deprecation warnings for %elim
569− | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics
570− deriving (Show, Eq, Generic)
571444
572−data REPLPort = DontListen | ListenPort PortNumber
573− deriving (Eq, Generic, Show)
445+
574446
575447-- Parsed declarations
576448
@@ -1177,6 +1049,7 @@ mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
11771049 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
11781050 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
11791051 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1052+ mapPDoFC (DoRewrite fc h) = DoRewrite (f fc) (mapPTermFC f g h)
11801053mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
11811054mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
11821055mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
@@ -1301,6 +1174,7 @@ data PDo' t = DoExp FC t
13011174 | DoBindP FC t t [(t,t)]
13021175 | DoLet FC Name FC t t -- ^ second FC is precise name location
13031176 | DoLetP FC t t
1177+ | DoRewrite FC t -- rewrite in do block
13041178 deriving (Eq, Ord, Functor, Data, Generic, Typeable)
13051179{-!
13061180deriving instance Binary PDo'
@@ -1312,6 +1186,7 @@ instance Sized a => Sized (PDo' a) where
13121186 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
13131187 size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
13141188 size (DoLetP fc l r) = 1 + size fc + size l + size r
1189+ size (DoRewrite fc h) = 1 + size fc + size h
13151190
13161191type PDo = PDo' PTerm
13171192
@@ -1407,6 +1282,7 @@ highestFC (PDoBlock lines) =
14071282 getDoFC (DoBindP fc l r alts) = fc
14081283 getDoFC (DoLet fc nm nfc l r) = fc
14091284 getDoFC (DoLetP fc l r) = fc
1285+ getDoFC (DoRewrite fc h) = fc
14101286
14111287highestFC (PIdiom fc _) = Just fc
14121288highestFC (PMetavar fc _) = Just fc
@@ -2081,6 +1957,9 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
20811957 ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab
20821958 text "no pretty printer for pattern-matching do binding" :
20831959 ppdo bnd dos
1960+ ppdo bnd (DoRewrite _ _ : dos) = -- ok because never made by delab
1961+ text "no pretty printer for pattern-matching do binding" :
1962+ ppdo bnd dos
20841963 ppdo _ [] = []
20851964 prettySe d p bnd (PCoerced t) = prettySe d p bnd t
20861965 prettySe d p bnd (PElabError s) = pretty s
src/Idris/Apropos.hs+1
@@ -5,6 +5,7 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8+{-# LANGUAGE FlexibleInstances #-}
89module Idris.Apropos (apropos, aproposModules) where
910
1011import Idris.AbsSyntax
src/Idris/CaseSplit.hs+1−1
@@ -17,7 +17,7 @@ Always take the "more specific" argument when there is a discrepancy, i.e.
1717names over '_', patterns over names, etc.
1818-}
1919
20−{-# LANGUAGE PatternGuards #-}
20+{-# LANGUAGE FlexibleContexts, PatternGuards #-}
2121
2222module Idris.CaseSplit(
2323 splitOnLine, replaceSplits
src/Idris/Chaser.hs+2
@@ -5,6 +5,8 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8+{-# LANGUAGE FlexibleContexts #-}
9+
810module Idris.Chaser(
911 buildTree, getImports
1012 , getModuleFiles
src/Idris/CmdOptions.hs+1−6
@@ -16,11 +16,8 @@ module Idris.CmdOptions
1616 , getPkgREPL, getPkgTest, getPort, getIBCSubDir
1717 ) where
1818
19−import Idris.AbsSyntax (getClient, getIBCSubDir, getPkg, getPkgCheck,
20− getPkgClean, getPkgMkDoc, getPkgREPL, getPkgTest,
21− getPort, opt)
22−import Idris.AbsSyntaxTree
2319import Idris.Info (getIdrisVersion)
20+import Idris.Options
2421import IRTS.CodegenCommon
2522
2623import Control.Monad.Trans (lift)
@@ -28,9 +25,7 @@ import Control.Monad.Trans.Except (throwE)
2825import Control.Monad.Trans.Reader (ask)
2926import Data.Char
3027import Data.Maybe
31−#if MIN_VERSION_optparse_applicative(0,13,0)
3228import Data.Monoid ((<>))
33−#endif
3429import Options.Applicative
3530import Options.Applicative.Arrows
3631import Options.Applicative.Types (ReadM(..))
src/Idris/Core/Binary.hs+2
@@ -5,6 +5,8 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8+{-# LANGUAGE FlexibleInstances #-}
9+
810{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
911module Idris.Core.Binary where
1012
src/Idris/Core/CaseTree.hs+2−2
@@ -18,8 +18,8 @@ allows casing on arbitrary terms, here we choose to maintain the distinction
1818in order to allow for better optimisation opportunities.
1919
2020-}
21−{-# LANGUAGE DeriveFunctor, DeriveGeneric, PatternGuards, TypeSynonymInstances
22− #-}
21+{-# LANGUAGE DeriveFunctor, DeriveGeneric, FlexibleContexts, FlexibleInstances,
22+ PatternGuards, TypeSynonymInstances #-}
2323
2424module Idris.Core.CaseTree (
2525 CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..), ErasureInfo
src/Idris/Core/DeepSeq.hs+4−1
@@ -5,7 +5,8 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8−{-# LANGUAGE BangPatterns, ViewPatterns #-}
8+{-# LANGUAGE BangPatterns, CPP, FlexibleInstances, TypeSynonymInstances,
9+ ViewPatterns #-}
910{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
1011
1112module Idris.Core.DeepSeq where
@@ -27,7 +28,9 @@ forceDefCtxt (force -> !ctxt) = ctxt
2728
2829instance NFData NameOutput
2930instance NFData TextFormatting
31+#if !(MIN_VERSION_base(4,10,0))
3032instance NFData Ordering
33+#endif
3134instance NFData OutputAnnotation
3235instance NFData SpecialName
3336instance NFData Universe
src/Idris/Core/ProofState.hs+2−1
@@ -10,7 +10,8 @@ proofs, and some high level commands for introducing new theorems,
1010evaluation/checking inside the proof system, etc.
1111-}
1212
13−{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, PatternGuards #-}
13+{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses,
14+ PatternGuards #-}
1415module Idris.Core.ProofState(
1516 ProofState(..), newProof, envAtFocus, goalAtFocus
1617 , Tactic(..), Goal(..), processTactic, nowElaboratingPS
src/Idris/Core/TT.hs+4−2
@@ -22,8 +22,10 @@ TT is the core language of Idris. The language has:
2222 * We have a simple collection of tactics which we use to elaborate source
2323 programs with implicit syntax into fully explicit terms.
2424-}
25−{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveGeneric, FlexibleContexts,
26− FunctionalDependencies, MultiParamTypeClasses, PatternGuards #-}
25+{-# LANGUAGE DeriveDataTypeable, DeriveFoldable, DeriveFunctor, DeriveGeneric,
26+ DeriveTraversable, FlexibleContexts, FlexibleInstances,
27+ FunctionalDependencies, MultiParamTypeClasses, PatternGuards,
28+ TypeSynonymInstances #-}
2729{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
2830module Idris.Core.TT(
2931 AppStatus(..), ArithTy(..), Binder(..), Const(..), Ctxt(..)
src/Idris/Core/Typecheck.hs+2−2
@@ -6,8 +6,8 @@ License : BSD3
66Maintainer : The Idris Community.
77-}
88
9−{-# LANGUAGE DeriveFunctor, FlexibleInstances, MultiParamTypeClasses,
10− PatternGuards #-}
9+{-# LANGUAGE DeriveFunctor, FlexibleContexts, FlexibleInstances,
10+ MultiParamTypeClasses, PatternGuards #-}
1111
1212module Idris.Core.Typecheck where
1313
src/Idris/Core/Unify.hs+1−1
@@ -11,7 +11,7 @@ Returns a list of hole names paired with the term which solves them, and
1111a list of things which need to be injective.
1212
1313-}
14−{-# LANGUAGE PatternGuards #-}
14+{-# LANGUAGE FlexibleContexts, PatternGuards #-}
1515
1616module Idris.Core.Unify(
1717 match_unify, unify
src/Idris/Core/WHNF.hs+1−1
@@ -6,7 +6,7 @@ License : BSD3
66Maintainer : The Idris Community.
77-}
88
9−{-# LANGUAGE PatternGuards #-}
9+{-# LANGUAGE FlexibleContexts, PatternGuards #-}
1010{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
1111module Idris.Core.WHNF(whnf, whnfArgs, WEnv) where
1212
src/Idris/Coverage.hs+1−1
@@ -5,7 +5,7 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8−{-# LANGUAGE PatternGuards #-}
8+{-# LANGUAGE FlexibleContexts, PatternGuards #-}
99module Idris.Coverage(genClauses, validCoverageCase, recoverableCoverage,
1010 mkPatTm) where
1111
src/Idris/DSL.hs+2
@@ -109,6 +109,8 @@ expandSugar dsl (PDoBlock ds)
109109 = PLet fc n nfc ty tm (block b rest)
110110 block b (DoLetP fc p tm : rest)
111111 = PCase fc tm [(p, block b rest)]
112+ block b (DoRewrite fc h : rest)
113+ = PRewrite fc Nothing h (block b rest) Nothing
112114 block b (DoExp fc tm : rest)
113115 = PApp fc b
114116 [pexp tm,
src/Idris/DataOpts.hs+1−1
@@ -5,7 +5,7 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8−{-# LANGUAGE PatternGuards #-}
8+{-# LANGUAGE FlexibleInstances, PatternGuards #-}
99
1010module Idris.DataOpts(applyOpts) where
1111
src/Idris/DeepSeq.hs+1
@@ -18,6 +18,7 @@ import Idris.Core.DeepSeq
1818import Idris.Core.TT
1919import Idris.Docstrings
2020import qualified Idris.Docstrings as D
21+import Idris.Options
2122import IRTS.CodegenCommon (OutputType(..))
2223import IRTS.Lang (PrimFn(..))
2324
src/Idris/Docs.hs+2−1
@@ -15,7 +15,7 @@ module Idris.Docs (
1515 , FunDoc, FunDoc'(..), Docs, Docs'(..)
1616 ) where
1717
18−import Idris.AbsSyntax (FixDecl(..), Fixity, HowMuchDocs(..), IState(..), Idris,
18+import Idris.AbsSyntax (FixDecl(..), Fixity, IState(..), Idris,
1919 InterfaceInfo(..), PArg'(..), PDecl'(..), PPOption(..),
2020 PTerm(..), Plicity(..), RecordInfo(..), basename,
2121 getIState, modDocName, ppOptionIst, pprintPTerm,
@@ -26,6 +26,7 @@ import Idris.Delaborate
2626import Idris.Docstrings (DocTerm, Docstring, emptyDocstring, noDocs,
2727 nullDocstring, overview, renderDocTerm,
2828 renderDocstring)
29+import Idris.Options (HowMuchDocs(..))
2930
3031import Util.Pretty
3132
src/Idris/Docstrings.hs+2−1
@@ -6,7 +6,8 @@ License : BSD3
66Maintainer : The Idris Community.
77-}
88
9−{-# LANGUAGE DeriveFunctor, DeriveGeneric, ScopedTypeVariables #-}
9+{-# LANGUAGE DeriveFoldable, DeriveFunctor, DeriveGeneric, DeriveTraversable,
10+ ScopedTypeVariables #-}
1011{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
1112module Idris.Docstrings (
1213 Docstring(..), Block(..), Inline(..), parseDocstring, renderDocstring
src/Idris/Elab/Clause.hs+1
@@ -31,6 +31,7 @@ import Idris.Elab.Utils
3131import Idris.Error
3232import Idris.Imports
3333import Idris.Inliner
34+import Idris.Options
3435import Idris.Output (iRenderResult, iWarn, iputStrLn, pshow, sendHighlighting)
3536import Idris.PartialEval
3637import Idris.Primitives
src/Idris/Elab/Provider.hs+1
@@ -30,6 +30,7 @@ import Idris.Elab.Value
3030import Idris.Error
3131import Idris.Imports
3232import Idris.Inliner
33+import Idris.Options
3334import Idris.Output (iWarn, iputStrLn, pshow)
3435import Idris.PartialEval
3536import Idris.Primitives
src/Idris/Elab/Quasiquote.hs+1
@@ -75,6 +75,7 @@ extractDoUnquotes d (DoLet fc n nfc v b)
7575 (b', ex2) <- extractUnquotes d b
7676 return (DoLet fc n nfc v' b', ex1 ++ ex2)
7777extractDoUnquotes d (DoLetP fc t t') = fail "Pattern-matching lets cannot be quasiquoted"
78+extractDoUnquotes d (DoRewrite fc h) = fail "Rewrites in Do block cannot be quasiquoted"
7879
7980
8081extractUnquotes :: Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
src/Idris/Elab/Term.hs+5−2
@@ -27,6 +27,7 @@ import Idris.Elab.Rewrite
2727import Idris.Elab.Utils
2828import Idris.Error
2929import Idris.ErrReverse (errReverse)
30+import Idris.Options
3031import Idris.Output (pshow)
3132import Idris.ProofSearch
3233import Idris.Reflection
@@ -2658,9 +2659,11 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
26582659 concat (intersperse ", " (map show handlers))
26592660 let reports = map (\n -> RApp (Var n) (reflectErr err)) handlers
26602661
2661− -- Typecheck error handlers - if this fails, then something else was wrong earlier!
2662+ -- Typecheck error handlers - if this fails, most
2663+ -- likely something which is needed by it has not
2664+ -- been imported, so keep the original error.
26622665 handlers <- case mapM (check (tt_ctxt ist) []) reports of
2663− Error e -> ierror $ ReflectionFailed "Type error while constructing reflected error" e
2666+ Error _ -> return [] -- ierror $ ReflectionFailed "Type error while constructing reflected error" e
26642667 OK hs -> return hs
26652668
26662669 -- Normalize error handler terms to produce the new messages
src/Idris/Elab/Type.hs+1
@@ -32,6 +32,7 @@ import Idris.Elab.Value
3232import Idris.Error
3333import Idris.Imports
3434import Idris.Inliner
35+import Idris.Options
3536import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
3637import Idris.PartialEval
3738import Idris.Primitives
src/Idris/Elab/Utils.hs+7−6
@@ -5,7 +5,7 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8−{-# LANGUAGE PatternGuards #-}
8+{-# LANGUAGE FlexibleContexts, PatternGuards #-}
99module Idris.Elab.Utils where
1010
1111import Idris.AbsSyntax
@@ -449,9 +449,12 @@ displayWarnings est
449449 = mapM_ displayImpWarning (implicit_warnings est)
450450 where
451451 displayImpWarning :: (FC, Name) -> Idris ()
452− displayImpWarning (fc, n) =
453− iputStrLn $ show fc ++ ":WARNING: " ++ show (nsroot n) ++ " is bound as an implicit\n"
454− ++ "\tDid you mean to refer to " ++ show n ++ "?"
452+ displayImpWarning (fc, n) = do
453+ ist <- getIState
454+ let msg = show (nsroot n)
455+ ++ " is bound as an implicit\n"
456+ ++ "\tDid you mean to refer to " ++ show n ++ "?"
457+ iWarn fc (pprintErr ist (Msg msg))
455458
456459propagateParams :: IState -> [Name] -> Type -> [Name] -> PTerm -> PTerm
457460propagateParams i ps t bound tm@(PApp _ (PRef fc hls n) args)
@@ -767,5 +770,3 @@ isPlausible ist var env n ty
767770 collectConstraints env tcs t
768771 | (V i, _) <- unApply t = (Just (env !! i), tcs)
769772 | otherwise = (Nothing, tcs)
770−
771−
src/Idris/ElabDecls.hs+1
@@ -41,6 +41,7 @@ import Idris.Elab.Value
4141import Idris.Error
4242import Idris.Imports
4343import Idris.Inliner
44+import Idris.Options
4445import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
4546import Idris.PartialEval
4647import Idris.Primitives
src/Idris/Erasure.hs+1
@@ -15,6 +15,7 @@ import Idris.Core.CaseTree
1515import Idris.Core.Evaluate
1616import Idris.Core.TT
1717import Idris.Error
18+import Idris.Options
1819import Idris.Primitives
1920
2021import Prelude hiding (id, (.))
src/Idris/Error.hs+1
@@ -138,6 +138,7 @@ warnDisamb ist (PDoBlock steps) = mapM_ wStep steps
138138 mapM_ (\(x,y) -> warnDisamb ist x >> warnDisamb ist y) cs
139139 wStep (DoLet _ _ _ x y) = warnDisamb ist x >> warnDisamb ist y
140140 wStep (DoLetP _ x y) = warnDisamb ist x >> warnDisamb ist y
141+ wStep (DoRewrite _ h) = warnDisamb ist h
141142warnDisamb ist (PIdiom _ x) = warnDisamb ist x
142143warnDisamb ist (PMetavar _ _) = return ()
143144warnDisamb ist (PProof tacs) = mapM_ (Foldable.mapM_ (warnDisamb ist)) tacs
src/Idris/IBC.hs+9−1
@@ -5,7 +5,7 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8−{-# LANGUAGE TypeSynonymInstances #-}
8+{-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}
99{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
1010
1111module Idris.IBC (loadIBC, loadPkgIndex,
@@ -23,6 +23,7 @@ import Idris.Docstrings (Docstring)
2323import qualified Idris.Docstrings as D
2424import Idris.Error
2525import Idris.Imports
26+import Idris.Options
2627import Idris.Output
2728import IRTS.System (getIdrisLibDir)
2829
@@ -2292,6 +2293,9 @@ instance (Binary t) => Binary (PDo' t) where
22922293 put x1
22932294 put x2
22942295 put x3
2296+ DoRewrite x1 x2 -> do putWord8 5
2297+ put x1
2298+ put x2
22952299 get
22962300 = do i <- getWord8
22972301 case i of
@@ -2318,6 +2322,10 @@ instance (Binary t) => Binary (PDo' t) where
23182322 x2 <- get
23192323 x3 <- get
23202324 return (DoLetP x1 x2 x3)
2325+ 5 -> do
2326+ x1 <- get
2327+ x2 <- get
2328+ return (DoRewrite x1 x2)
23212329 _ -> error "Corrupted binary data for PDo'"
23222330
23232331
src/Idris/IdrisDoc.hs+2
@@ -18,6 +18,7 @@ import Idris.Core.TT (Name(..), OutputAnnotation(..), SpecialName(..),
1818import Idris.Docs
1919import Idris.Docstrings (nullDocstring)
2020import qualified Idris.Docstrings as Docstrings
21+import Idris.Options
2122import Idris.Parser.Helpers (opChars)
2223import IRTS.System (getIdrisDataFileByName)
2324
@@ -343,6 +344,7 @@ extractPDo (DoBindP _ p1 p2 ps) = let (ps1, ps2) = unzip ps
343344 in concatMap extract (p1 : p2 : ps')
344345extractPDo (DoLet _ n _ p1 p2) = n : concatMap extract [p1, p2]
345346extractPDo (DoLetP _ p1 p2) = concatMap extract [p1, p2]
347+extractPDo (DoRewrite _ p) = extract p
346348
347349-- | Helper function for extractPTermNames
348350extractPTactic :: PTactic -> [Name]
src/Idris/Info.hs+1−1
@@ -25,8 +25,8 @@ module Idris.Info
2525 , getIdrisDataFileByName
2626 ) where
2727
28−import Idris.AbsSyntax (loggingCatsStr)
2928import Idris.Imports (installedPackages)
29+import Idris.Options (loggingCatsStr)
3030import qualified IRTS.System as S
3131
3232import Paths_idris
src/Idris/Interactive.hs+14−16
@@ -37,7 +37,7 @@ import System.IO
3737
3838caseSplitAt :: FilePath -> Bool -> Int -> Name -> Idris ()
3939caseSplitAt fn updatefile l n
40− = do src <- runIO $ readSource fn
40+ = do src <- runIO $ readSourceStrict fn
4141 (ok, res) <- splitOnLine l n fn
4242 logLvl 1 (showSep "\n" (map show res))
4343 let (before, (ap : later)) = splitAt (l-1) (lines src)
@@ -61,7 +61,7 @@ addClauseFrom fn updatefile l n = do
6161 case metavars of
6262 Nothing -> addMissing fn updatefile l n
6363 Just _ -> do
64− src <- runIO $ readSource fn
64+ src <- runIO $ readSourceStrict fn
6565 let (before, tyline : later) = splitAt (l-1) (lines src)
6666 let indent = getIndent 0 (show n) tyline
6767 cl <- getClause l fulln n fn
@@ -88,7 +88,7 @@ addClauseFrom fn updatefile l n = do
8888
8989addProofClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()
9090addProofClauseFrom fn updatefile l n
91− = do src <- runIO $ readSource fn
91+ = do src <- runIO $ readSourceStrict fn
9292 let (before, tyline : later) = splitAt (l-1) (lines src)
9393 let indent = getIndent 0 (show n) tyline
9494 cl <- getProofClause l n fn
@@ -109,9 +109,9 @@ addProofClauseFrom fn updatefile l n
109109
110110addMissing :: FilePath -> Bool -> Int -> Name -> Idris ()
111111addMissing fn updatefile l n
112− = do src <- runIO $ readSource fn
112+ = do src <- runIO $ readSourceStrict fn
113113 let (before, tyline : later) = splitAt (l-1) (lines src)
114− let indent = getIndent 0 (show n) tyline
114+ let indent = getIndent tyline
115115 i <- getIState
116116 cl <- getInternalApp fn l
117117 let n' = getAppName cl
@@ -124,10 +124,10 @@ addMissing fn updatefile l n
124124 if updatefile
125125 then do let fb = fn ++ "~"
126126 runIO $ writeSource fb (unlines (before ++ nonblank)
127− ++ extras ++
128− (if null extras then ""
129− else "\n" ++ unlines rest))
130− runIO $ copyFile fb fn
127+ ++ extras
128+ ++ (if null extras then "" else "\n")
129+ ++ unlines rest)
130+ runIO $ (length src `seq` copyFile fb fn)
131131 else iPrintResult extras
132132 where showPat = show . stripNS
133133 stripNS tm = mapPT dens tm where
@@ -155,14 +155,12 @@ addMissing fn updatefile l n
155155 "\n" ++ rest))
156156 showNew nm i _ [] = return ""
157157
158− getIndent i n [] = 0
159− getIndent i n xs | take (length n) xs == n = i
160− getIndent i n (x : xs) = getIndent (i + 1) n xs
158+ getIndent s = length (takeWhile isSpace s)
161159
162160
163161makeWith :: FilePath -> Bool -> Int -> Name -> Idris ()
164162makeWith fn updatefile l n = do
165− src <- runIO $ readSource fn
163+ src <- runIO $ readSourceStrict fn
166164 i <- getIState
167165 indentWith <- getIndentWith
168166 let (before, tyline : later) = splitAt (l-1) (lines src)
@@ -186,7 +184,7 @@ makeWith fn updatefile l n = do
186184-- block, using a _ for the scrutinee
187185makeCase :: FilePath -> Bool -> Int -> Name -> Idris ()
188186makeCase fn updatefile l n
189− = do src <- runIO $ readSource fn
187+ = do src <- runIO $ readSourceStrict fn
190188 let (before, tyline : later) = splitAt (l-1) (lines src)
191189 let newcase = addCaseSkel (show n) tyline
192190
@@ -226,7 +224,7 @@ doProofSearch :: FilePath -> Bool -> Bool ->
226224doProofSearch fn updatefile rec l n hints Nothing
227225 = doProofSearch fn updatefile rec l n hints (Just 20)
228226doProofSearch fn updatefile rec l n hints (Just depth)
229− = do src <- runIO $ readSource fn
227+ = do src <- runIO $ readSourceStrict fn
230228 let (before, tyline : later) = splitAt (l-1) (lines src)
231229 ctxt <- getContext
232230 mn <- case lookupNames n ctxt of
@@ -321,7 +319,7 @@ addBracket True new | any isSpace new = '(' : new ++ ")"
321319
322320makeLemma :: FilePath -> Bool -> Int -> Name -> Idris ()
323321makeLemma fn updatefile l n
324− = do src <- runIO $ readSource fn
322+ = do src <- runIO $ readSourceStrict fn
325323 let (before, tyline : later) = splitAt (l-1) (lines src)
326324
327325 -- if the name is in braces, rather than preceded by a ?, treat it
src/Idris/Main.hs+1
@@ -22,6 +22,7 @@ import Idris.Error
2222import Idris.IBC
2323import Idris.Info
2424import Idris.ModeCommon
25+import Idris.Options
2526import Idris.Output
2627import Idris.Parser hiding (indent)
2728import Idris.REPL
src/Idris/ModeCommon.hs+1
@@ -15,6 +15,7 @@ import Idris.Error
1515import Idris.IBC
1616import Idris.Imports
1717import Idris.Info
18+import Idris.Options
1819import Idris.Output
1920import Idris.Parser hiding (indent)
2021import IRTS.Exports
src/Idris/Options.hsnew file+283
@@ -0,0 +1,283 @@
1+{-|
2+Module : Idris.Options
3+Description : Compiler options for Idris.
4+Copyright :
5+License : BSD3
6+Maintainer : The Idris Community.
7+-}
8+{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveGeneric, PatternGuards #-}
9+
10+module Idris.Options where
11+
12+import Data.Maybe
13+import GHC.Generics (Generic)
14+import IRTS.CodegenCommon (OutputType)
15+import Network.Socket (PortNumber)
16+
17+data Opt = Filename String
18+ | Quiet
19+ | NoBanner
20+ | ColourREPL Bool
21+ | Idemode
22+ | IdemodeSocket
23+ | IndentWith Int
24+ | IndentClause Int
25+ | ShowAll
26+ | ShowLibs
27+ | ShowLibDir
28+ | ShowDocDir
29+ | ShowIncs
30+ | ShowPkgs
31+ | ShowLoggingCats
32+ | NoBasePkgs
33+ | NoPrelude
34+ | NoBuiltins -- only for the really primitive stuff!
35+ | NoREPL
36+ | OLogging Int
37+ | OLogCats [LogCat]
38+ | Output String
39+ | Interface
40+ | TypeCase
41+ | TypeInType
42+ | DefaultTotal
43+ | DefaultPartial
44+ | WarnPartial
45+ | WarnReach
46+ | AuditIPkg
47+ | EvalTypes
48+ | NoCoverage
49+ | ErrContext
50+ | ShowImpl
51+ | Verbose Int
52+ | Port REPLPort -- ^ REPL TCP port
53+ | IBCSubDir String
54+ | ImportDir String
55+ | SourceDir String
56+ | PkgBuild String
57+ | PkgInstall String
58+ | PkgClean String
59+ | PkgCheck String
60+ | PkgREPL String
61+ | PkgDocBuild String -- IdrisDoc
62+ | PkgDocInstall String
63+ | PkgTest String
64+ | PkgIndex FilePath
65+ | WarnOnly
66+ | Pkg String
67+ | BCAsm String
68+ | DumpDefun String
69+ | DumpCases String
70+ | UseCodegen Codegen
71+ | CodegenArgs String
72+ | OutputTy OutputType
73+ | Extension LanguageExt
74+ | InterpretScript String
75+ | EvalExpr String
76+ | TargetTriple String
77+ | TargetCPU String
78+ | OptLevel Int
79+ | AddOpt Optimisation
80+ | RemoveOpt Optimisation
81+ | Client String
82+ | ShowOrigErr
83+ | AutoWidth -- ^ Automatically adjust terminal width
84+ | AutoSolve -- ^ Automatically issue "solve" tactic in old-style interactive prover
85+ | UseConsoleWidth ConsoleWidth
86+ | DumpHighlights
87+ | DesugarNats
88+ | NoElimDeprecationWarnings -- ^ Don't show deprecation warnings for %elim
89+ | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics
90+ deriving (Show, Eq, Generic)
91+
92+
93+data REPLPort = DontListen | ListenPort PortNumber
94+ deriving (Eq, Generic, Show)
95+
96+
97+data Codegen = Via IRFormat String
98+ | Bytecode
99+ deriving (Show, Eq, Generic)
100+
101+
102+data LanguageExt = TypeProviders | ErrorReflection | UniquenessTypes
103+ | DSLNotation | ElabReflection | FCReflection
104+ | LinearTypes
105+ deriving (Show, Eq, Read, Ord, Generic)
106+
107+data IRFormat = IBCFormat | JSONFormat deriving (Show, Eq, Generic)
108+
109+
110+-- | How wide is the console?
111+data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken
112+ | ColsWide Int -- ^ Manually specified - must be positive
113+ | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise
114+ deriving (Show, Eq, Generic)
115+
116+data HowMuchDocs = FullDocs | OverviewDocs
117+
118+data OutputFmt = HTMLOutput | LaTeXOutput
119+
120+data Optimisation = PETransform -- ^ partial eval and associated transforms
121+ deriving (Show, Eq, Generic)
122+
123+-- | Recognised logging categories for the Idris compiler.
124+--
125+-- @TODO add in sub categories.
126+data LogCat = IParse
127+ | IElab
128+ | ICodeGen
129+ | IErasure
130+ | ICoverage
131+ | IIBC
132+ deriving (Show, Eq, Ord, Generic)
133+
134+strLogCat :: LogCat -> String
135+strLogCat IParse = "parser"
136+strLogCat IElab = "elab"
137+strLogCat ICodeGen = "codegen"
138+strLogCat IErasure = "erasure"
139+strLogCat ICoverage = "coverage"
140+strLogCat IIBC = "ibc"
141+
142+codegenCats :: [LogCat]
143+codegenCats = [ICodeGen]
144+
145+parserCats :: [LogCat]
146+parserCats = [IParse]
147+
148+elabCats :: [LogCat]
149+elabCats = [IElab]
150+
151+loggingCatsStr :: String
152+loggingCatsStr = unlines
153+ [ (strLogCat IParse)
154+ , (strLogCat IElab)
155+ , (strLogCat ICodeGen)
156+ , (strLogCat IErasure)
157+ , (strLogCat ICoverage)
158+ , (strLogCat IIBC)
159+ ]
160+
161+getFile :: Opt -> Maybe String
162+getFile (Filename s) = Just s
163+getFile _ = Nothing
164+
165+getBC :: Opt -> Maybe String
166+getBC (BCAsm s) = Just s
167+getBC _ = Nothing
168+
169+getOutput :: Opt -> Maybe String
170+getOutput (Output s) = Just s
171+getOutput _ = Nothing
172+
173+getIBCSubDir :: Opt -> Maybe String
174+getIBCSubDir (IBCSubDir s) = Just s
175+getIBCSubDir _ = Nothing
176+
177+getImportDir :: Opt -> Maybe String
178+getImportDir (ImportDir s) = Just s
179+getImportDir _ = Nothing
180+
181+getSourceDir :: Opt -> Maybe String
182+getSourceDir (SourceDir s) = Just s
183+getSourceDir _ = Nothing
184+
185+getPkgDir :: Opt -> Maybe String
186+getPkgDir (Pkg s) = Just s
187+getPkgDir _ = Nothing
188+
189+getPkg :: Opt -> Maybe (Bool, String)
190+getPkg (PkgBuild s) = Just (False, s)
191+getPkg (PkgInstall s) = Just (True, s)
192+getPkg _ = Nothing
193+
194+getPkgClean :: Opt -> Maybe String
195+getPkgClean (PkgClean s) = Just s
196+getPkgClean _ = Nothing
197+
198+getPkgREPL :: Opt -> Maybe String
199+getPkgREPL (PkgREPL s) = Just s
200+getPkgREPL _ = Nothing
201+
202+getPkgCheck :: Opt -> Maybe String
203+getPkgCheck (PkgCheck s) = Just s
204+getPkgCheck _ = Nothing
205+
206+-- | Returns None if given an Opt which is not PkgMkDoc
207+-- Otherwise returns Just x, where x is the contents of PkgMkDoc
208+getPkgMkDoc :: Opt -- ^ Opt to extract
209+ -> Maybe (Bool, String) -- ^ Result
210+getPkgMkDoc (PkgDocBuild str) = Just (False,str)
211+getPkgMkDoc (PkgDocInstall str) = Just (True,str)
212+getPkgMkDoc _ = Nothing
213+
214+getPkgTest :: Opt -- ^ the option to extract
215+ -> Maybe String -- ^ the package file to test
216+getPkgTest (PkgTest f) = Just f
217+getPkgTest _ = Nothing
218+
219+getCodegen :: Opt -> Maybe Codegen
220+getCodegen (UseCodegen x) = Just x
221+getCodegen _ = Nothing
222+
223+getCodegenArgs :: Opt -> Maybe String
224+getCodegenArgs (CodegenArgs args) = Just args
225+getCodegenArgs _ = Nothing
226+
227+getConsoleWidth :: Opt -> Maybe ConsoleWidth
228+getConsoleWidth (UseConsoleWidth x) = Just x
229+getConsoleWidth _ = Nothing
230+
231+getExecScript :: Opt -> Maybe String
232+getExecScript (InterpretScript expr) = Just expr
233+getExecScript _ = Nothing
234+
235+getPkgIndex :: Opt -> Maybe FilePath
236+getPkgIndex (PkgIndex file) = Just file
237+getPkgIndex _ = Nothing
238+
239+getEvalExpr :: Opt -> Maybe String
240+getEvalExpr (EvalExpr expr) = Just expr
241+getEvalExpr _ = Nothing
242+
243+getOutputTy :: Opt -> Maybe OutputType
244+getOutputTy (OutputTy t) = Just t
245+getOutputTy _ = Nothing
246+
247+getLanguageExt :: Opt -> Maybe LanguageExt
248+getLanguageExt (Extension e) = Just e
249+getLanguageExt _ = Nothing
250+
251+getTriple :: Opt -> Maybe String
252+getTriple (TargetTriple x) = Just x
253+getTriple _ = Nothing
254+
255+getCPU :: Opt -> Maybe String
256+getCPU (TargetCPU x) = Just x
257+getCPU _ = Nothing
258+
259+getOptLevel :: Opt -> Maybe Int
260+getOptLevel (OptLevel x) = Just x
261+getOptLevel _ = Nothing
262+
263+getOptimisation :: Opt -> Maybe (Bool,Optimisation)
264+getOptimisation (AddOpt p) = Just (True, p)
265+getOptimisation (RemoveOpt p) = Just (False, p)
266+getOptimisation _ = Nothing
267+
268+getColour :: Opt -> Maybe Bool
269+getColour (ColourREPL b) = Just b
270+getColour _ = Nothing
271+
272+getClient :: Opt -> Maybe String
273+getClient (Client x) = Just x
274+getClient _ = Nothing
275+
276+-- Get the first valid port
277+getPort :: [Opt] -> Maybe REPLPort
278+getPort [] = Nothing
279+getPort (Port p : _ ) = Just p
280+getPort (_ : xs) = getPort xs
281+
282+opt :: (Opt -> Maybe a) -> [Opt] -> [a]
283+opt = mapMaybe
src/Idris/Output.hs+2
@@ -6,6 +6,7 @@ License : BSD3
66Maintainer : The Idris Community.
77-}
88
9+{-# LANGUAGE FlexibleInstances #-}
910{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
1011
1112module Idris.Output where
@@ -17,6 +18,7 @@ import Idris.Core.TT
1718import Idris.Delaborate
1819import Idris.Docstrings
1920import Idris.IdeMode
21+import Idris.Options
2022
2123import Util.Pretty
2224import Util.ScreenSize (getScreenWidth)
src/Idris/Package.hs+1−1
@@ -35,7 +35,7 @@ import Idris.IBC
3535import Idris.IdrisDoc
3636import Idris.Imports
3737import Idris.Main (idris, idrisMain)
38−import Idris.Output (pshow)
38+import Idris.Options
3939import Idris.Output
4040import Idris.Parser (loadModule)
4141import Idris.REPL
src/Idris/Package/Common.hs+1−1
@@ -6,8 +6,8 @@ Maintainer : The Idris Community.
66-}
77module Idris.Package.Common where
88
9−import Idris.AbsSyntaxTree (Opt(..))
109import Idris.Core.TT (Name)
10+import Idris.Options (Opt(..))
1111
1212-- | Description of an Idris package.
1313data PkgDesc = PkgDesc {
src/Idris/Package/Parser.hs+17−13
@@ -5,10 +5,7 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8−{-# LANGUAGE CPP, ConstraintKinds #-}
9−#if !(MIN_VERSION_base(4,8,0))
10−{-# LANGUAGE OverlappingInstances #-}
11−#endif
8+{-# LANGUAGE CPP, ConstraintKinds, FlexibleInstances, TypeSynonymInstances #-}
129module Idris.Package.Parser where
1310
1411import Idris.AbsSyntaxTree
@@ -24,7 +21,9 @@ import Control.Applicative
2421import Control.Monad.State.Strict
2522import Data.List (union)
2623import Data.Maybe (fromJust, isNothing)
27−import System.FilePath (isValid, takeFileName)
24+import System.Directory (doesFileExist)
25+import System.Exit
26+import System.FilePath (isValid, takeExtension, takeFileName)
2827import qualified Text.PrettyPrint.ANSI.Leijen as PP
2928import Text.Trifecta hiding (char, charLiteral, natural, span, string, symbol,
3029 whiteSpace)
@@ -48,20 +47,25 @@ instance {-# OVERLAPPING #-} DeltaParsing PParser where
4847 {-# INLINE restOfLine #-}
4948#endif
5049
51−#if MIN_VERSION_base(4,8,0)
5250instance {-# OVERLAPPING #-} TokenParsing PParser where
53−#else
54−instance TokenParsing PParser where
55−#endif
5651 someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()
5752
5853
5954parseDesc :: FilePath -> IO PkgDesc
6055parseDesc fp = do
61− p <- readFile fp
62− case runparser pPkg defaultPkg fp p of
63− Failure (ErrInfo err _) -> fail (show $ PP.plain err)
64− Success x -> return x
56+ when (not $ takeExtension fp == ".ipkg") $ do
57+ putStrLn $ unwords ["The presented iPKG file does not have a '.ipkg' extension:", show fp]
58+ exitWith (ExitFailure 1)
59+ res <- doesFileExist fp
60+ if res
61+ then do
62+ p <- readFile fp
63+ case runparser pPkg defaultPkg fp p of
64+ Failure (ErrInfo err _) -> fail (show $ PP.plain err)
65+ Success x -> return x
66+ else do
67+ putStrLn $ unwords [ "The presented iPKG file does not exist:", show fp]
68+ exitWith (ExitFailure 1)
6569
6670pPkg :: PParser PkgDesc
6771pPkg = do
src/Idris/Parser.hs+8−2
@@ -5,7 +5,8 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8−{-# LANGUAGE ConstraintKinds, GeneralizedNewtypeDeriving, PatternGuards #-}
8+{-# LANGUAGE ConstraintKinds, FlexibleContexts, GeneralizedNewtypeDeriving,
9+ PatternGuards #-}
910{-# OPTIONS_GHC -O0 #-}
1011module Idris.Parser(module Idris.Parser,
1112 module Idris.Parser.Expr,
@@ -26,6 +27,7 @@ import Idris.ElabDecls
2627import Idris.Error
2728import Idris.IBC
2829import Idris.Imports
30+import Idris.Options
2931import Idris.Output
3032import Idris.Parser.Data
3133import Idris.Parser.Expr
@@ -1568,7 +1570,8 @@ parseImports fname input
15681570 [ImportInfo],
15691571 Maybe Delta),
15701572 [(FC, OutputAnnotation)], IState)
1571− imports = do whiteSpace
1573+ imports = do optional shebang
1574+ whiteSpace
15721575 (mdoc, mname, annots) <- moduleHeader
15731576 ps_exp <- many import_
15741577 mrk <- mark
@@ -1593,6 +1596,9 @@ parseImports fname input
15931596 (fc, AnnNamespace ns (Just path)) : addPath annots path
15941597 addPath (annot:annots) path = annot : addPath annots path
15951598
1599+ shebang :: IdrisParser ()
1600+ shebang = string "#!" *> many (satisfy $ not . isEol) *> eol *> pure ()
1601+
15961602-- | There should be a better way of doing this...
15971603findFC :: Doc -> (FC, String)
15981604findFC x = let s = show (plain x) in findFC' s
src/Idris/Parser/Data.hs+1
@@ -13,6 +13,7 @@ import Idris.Core.Evaluate
1313import Idris.Core.TT
1414import Idris.Docstrings
1515import Idris.DSL
16+import Idris.Options
1617import Idris.Parser.Expr
1718import Idris.Parser.Helpers
1819import Idris.Parser.Ops
src/Idris/Parser/Expr.hs+8
@@ -12,6 +12,7 @@ module Idris.Parser.Expr where
1212import Idris.AbsSyntax
1313import Idris.Core.TT
1414import Idris.DSL
15+import Idris.Options
1516import Idris.Parser.Helpers
1617import Idris.Parser.Ops
1718
@@ -233,6 +234,7 @@ updateSynMatch = update
233234 = DoBindP fc (update ns i) (update ns t)
234235 (map (\(l,r) -> (update ns l, update ns r)) ts)
235236 upd ns (DoLetP fc i t) = DoLetP fc (update ns i) (update ns t)
237+ upd ns (DoRewrite fc h) = DoRewrite fc (update ns h)
236238 update ns (PIdiom fc t) = PIdiom fc $ update ns t
237239 update ns (PMetavar fc n) = uncurry (flip PMetavar) $ updateB ns (n, fc)
238240 update ns (PProof tacs) = PProof $ map (updTactic ns) tacs
@@ -1342,6 +1344,7 @@ doBlock syn
13421344Do ::=
13431345 'let' Name TypeSig'? '=' Expr
13441346 | 'let' Expr' '=' Expr
1347+ | 'rewrite Expr
13451348 | Name '<-' Expr
13461349 | Expr' '<-' Expr
13471350 | Expr
@@ -1366,6 +1369,11 @@ do_ syn
13661369 sc <- expr syn
13671370 highlightP kw AnnKeyword
13681371 return (DoLetP fc i sc))
1372+ <|> try (do kw <- reservedFC "rewrite"
1373+ fc <- getFC
1374+ sc <- expr syn
1375+ highlightP kw AnnKeyword
1376+ return (DoRewrite fc sc))
13691377 <|> try (do (i, ifc) <- name
13701378 symbol "<-"
13711379 fc <- getFC
src/Idris/Parser/Helpers.hs+4−9
@@ -5,11 +5,9 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8−{-# LANGUAGE CPP, ConstraintKinds, GeneralizedNewtypeDeriving, PatternGuards,
9− StandaloneDeriving #-}
10−#if !(MIN_VERSION_base(4,8,0))
11−{-# LANGUAGE OverlappingInstances #-}
12−#endif
8+{-# LANGUAGE CPP, ConstraintKinds, FlexibleInstances,
9+ GeneralizedNewtypeDeriving, PatternGuards, StandaloneDeriving,
10+ TypeSynonymInstances #-}
1311module Idris.Parser.Helpers where
1412
1513import Idris.AbsSyntax
@@ -17,6 +15,7 @@ import Idris.Core.Evaluate
1715import Idris.Core.TT
1816import Idris.Delaborate (pprintErr)
1917import Idris.Docstrings
18+import Idris.Options
2019import Idris.Output (iWarn)
2120
2221import qualified Util.Pretty as Pretty (text)
@@ -69,11 +68,7 @@ instance {-# OVERLAPPING #-} DeltaParsing IdrisParser where
6968
7069#endif
7170
72−#if MIN_VERSION_base(4,8,0)
7371instance {-# OVERLAPPING #-} TokenParsing IdrisParser where
74−#else
75−instance TokenParsing IdrisParser where
76−#endif
7772 someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()
7873 token p = do s <- get
7974 (FC fn (sl, sc) _) <- getFC --TODO: Update after fixing getFC
src/Idris/Parser/Ops.hs+2−1
@@ -5,7 +5,8 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8−{-# LANGUAGE ConstraintKinds, GeneralizedNewtypeDeriving, PatternGuards #-}
8+{-# LANGUAGE ConstraintKinds, FlexibleContexts, GeneralizedNewtypeDeriving,
9+ PatternGuards #-}
910module Idris.Parser.Ops where
1011
1112import Idris.AbsSyntax
src/Idris/PartialEval.hs+1−1
@@ -5,7 +5,7 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8−{-# LANGUAGE PatternGuards #-}
8+{-# LANGUAGE FlexibleContexts, PatternGuards #-}
99
1010module Idris.PartialEval(
1111 partial_eval, getSpecApps, specType
src/Idris/Prover.hs+2
@@ -32,6 +32,7 @@ import Idris.Elab.Value
3232import Idris.ElabDecls
3333import Idris.Error
3434import qualified Idris.IdeMode as IdeMode
35+import Idris.Options
3536import Idris.Output
3637import Idris.Parser hiding (params)
3738import Idris.TypeSearch (searchByType)
@@ -349,6 +350,7 @@ elabloop info fn d prompt prf e prev h env
349350 Success (Right cmd') ->
350351 case cmd' of
351352 DoLetP {} -> ifail "Pattern-matching let not supported here"
353+ DoRewrite {} -> ifail "Pattern-matching do-rewrite not supported here"
352354 DoBindP {} -> ifail "Pattern-matching <- not supported here"
353355 DoLet fc i ifc Placeholder expr ->
354356 do (tm, ty) <- elabVal (recinfo proverfc) ERHS (inLets ist env expr)
src/Idris/REPL.hs+2−1
@@ -5,7 +5,7 @@ License : BSD3
55Maintainer : The Idris Community.
66-}
77
8−{-# LANGUAGE PatternGuards #-}
8+{-# LANGUAGE FlexibleContexts, PatternGuards #-}
99
1010module Idris.REPL
1111 ( idemodeStart
@@ -68,6 +68,7 @@ import Idris.Info
6868import Idris.Inliner
6969import Idris.Interactive
7070import Idris.ModeCommon
71+import Idris.Options
7172import Idris.Output
7273import Idris.Parser hiding (indent)
7374import Idris.Prover
src/Idris/REPL/Commands.hs+1
@@ -3,6 +3,7 @@ module Idris.REPL.Commands where
33import Idris.AbsSyntaxTree
44import Idris.Colours
55import Idris.Core.TT
6+import Idris.Options
67
78-- | REPL commands
89data Command = Quit
src/Idris/REPL/Parser.hs+1
@@ -15,6 +15,7 @@ import Idris.AbsSyntax
1515import Idris.Colours
1616import Idris.Core.TT
1717import Idris.Help
18+import Idris.Options
1819import qualified Idris.Parser as P
1920import Idris.REPL.Commands
2021
src/Idris/Reflection.hs−5
@@ -21,11 +21,6 @@ import Idris.AbsSyntaxTree (ArgOpt(..), ElabD, Fixity(..), IState(idris_datatype
2121 initEState, pairCon, pairTy)
2222import Idris.Delaborate (delab)
2323
24−#if __GLASGOW_HASKELL__ < 710
25−import Control.Applicative (pure, (<$>), (<*>))
26−import Data.Traversable (mapM)
27−import Prelude hiding (mapM)
28−#endif
2924import Control.Monad (liftM, liftM2, liftM4)
3025import Control.Monad.State.Strict (lift)
3126import Data.List (findIndex, (\\))
src/Idris/Termination.hs+1
@@ -14,6 +14,7 @@ import Idris.Core.Evaluate
1414import Idris.Core.TT
1515import Idris.Delaborate
1616import Idris.Error
17+import Idris.Options
1718import Idris.Output (iWarn, iputStrLn)
1819
1920import Control.Monad.State.Strict
src/Util/Pretty.hs+3
@@ -5,6 +5,9 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8+
9+{-# LANGUAGE MultiParamTypeClasses #-}
10+
811module Util.Pretty (
912 module Text.PrettyPrint.Annotated.Leijen
1013 , Sized(..)
src/Util/System.hs+10
@@ -14,6 +14,7 @@ module Util.System( tempfile
1414 , writeSource
1515 , writeSourceText
1616 , readSource
17+ , readSourceStrict
1718 , setupBundledCC
1819 , isATTY
1920 ) where
@@ -60,6 +61,15 @@ readSource f = do h <- openFile f ReadMode
6061 hSetEncoding h utf8
6162 hGetContents h
6263
64+-- | Read a source file, make sure that the it all has been read before exiting the function.
65+-- | This is useful when we want to write the file again and need it to be closed.
66+readSourceStrict :: FilePath -> IO String
67+readSourceStrict f = withFile f ReadMode $
68+ \h -> do
69+ hSetEncoding h utf8
70+ src <- hGetContents h
71+ length src `seq` return src
72+
6373-- | Write a source file, same as writeFile except the encoding is set to utf-8
6474writeSource :: FilePath -> String -> IO ()
6575writeSource f s = withFile f WriteMode (\h -> hSetEncoding h utf8 >> hPutStr h s)
stack-shell.nix+1−1
@@ -2,7 +2,7 @@ with (import <nixpkgs> {});
22
33let
44 # MUST match resolver in stack.yaml
5− resolver = haskell.packages.lts-8_06.ghc;
5+ resolver = haskell.packages.lts-9_0.ghc;
66
77 native_libs = [
88 libffi
stack.yaml+1−1
@@ -1,4 +1,4 @@
1−resolver: lts-8.06
1+resolver: lts-9.0
22
33packages:
44 - location: .
test/TestData.hs+5−2
@@ -155,7 +155,9 @@ testFamiliesData = [
155155 ( 11, ANY ),
156156 ( 12, ANY ),
157157 ( 13, ANY ),
158− ( 14, C_CG )]),
158+ ( 14, C_CG ),
159+ ( 15, ANY ),
160+ ( 16, ANY )]),
159161 ("interfaces", "Interfaces",
160162 [ ( 1, ANY ),
161163 ( 2, ANY ),
@@ -256,7 +258,8 @@ testFamiliesData = [
256258 ( 77, ANY )]),
257259 ("regression", "Regression",
258260 [ ( 1 , ANY ),
259− ( 2 , ANY )]),
261+ ( 2 , ANY ),
262+ ( 3 , ANY )]),
260263 ("sourceLocation", "Source location",
261264 [ ( 1 , ANY )]),
262265 ("sugar", "Syntactic sugar",
test/TestRun.hs−2
@@ -7,9 +7,7 @@ import Control.Monad
77import Data.Char (isLetter)
88import qualified Data.IntMap as IMap
99import Data.List
10−#if MIN_VERSION_optparse_applicative(0,13,0)
1110import Data.Monoid ((<>))
12−#endif
1311import Data.Proxy
1412import Data.Typeable
1513import Options.Applicative
test/basic009/expected+1−1
@@ -1,5 +1,5 @@
11MAIN-PASS
2−Faulty.idr:6:9-12:WARNING: num is bound as an implicit
2+Faulty.idr:6:9-12:num is bound as an implicit
33 Did you mean to refer to A.num?
44Faulty.idr:7:7:When checking right hand side of fault with expected type
55 num = 0
test/basic018/expected+4−2
@@ -1,6 +1,8 @@
1−basic018.idr:7:12-17:WARNING: thing is bound as an implicit
1+basic018.idr:7:12-17:
2+thing is bound as an implicit
23 Did you mean to refer to Main.thing?
3−basic018.idr:12:8-13:WARNING: thing is bound as an implicit
4+basic018.idr:12:8-13:
5+thing is bound as an implicit
46 Did you mean to refer to Main.thing?
57basic018.idr:13:6:When checking right hand side of test with expected type
68 thing = S 41
test/interactive015/expectednew file+6
@@ -0,0 +1,6 @@
1+test (Just x) = ?Nothing_rhs_1
2+
3+test : Maybe a -> Bool
4+test Nothing = False
5+test (Just x) = ?Nothing_rhs_1
6+
test/interactive015/inputnew file+2
@@ -0,0 +1,2 @@
1+:addmissing 3 Nothing
2+:addmissing! 3 Nothing
test/interactive015/runnew file+8
@@ -0,0 +1,8 @@
1+#!/usr/bin/env bash
2+
3+cp src/interactive015.idr .
4+${IDRIS:-idris} "$@" --quiet --port none interactive015.idr < input
5+
6+cat interactive015.idr
7+
8+rm -f *.ibc interactive015.idr
test/interactive015/src/interactive015.idrnew file+4
@@ -0,0 +1,4 @@
1+
2+test : Maybe a -> Bool
3+test Nothing = False
4+
test/interactive016/expectednew file+7
@@ -0,0 +1,7 @@
1+
2+test : Maybe a -> Bool
3+test Nothing = False
4+test (Just x) = True
5+
6+other : Int
7+other = 3
test/interactive016/inputnew file+2
@@ -0,0 +1,2 @@
1+:addmissing 3 Nothing
2+:addmissing! 3 Nothing
test/interactive016/runnew file+8
@@ -0,0 +1,8 @@
1+#!/usr/bin/env bash
2+
3+cp src/interactive016.idr .
4+${IDRIS:-idris} "$@" --quiet --port none interactive016.idr < input
5+
6+cat interactive016.idr
7+
8+rm -f *.ibc interactive016.idr
test/interactive016/src/interactive016.idrnew file+7
@@ -0,0 +1,7 @@
1+
2+test : Maybe a -> Bool
3+test Nothing = False
4+test (Just x) = True
5+
6+other : Int
7+other = 3
test/interactive017/TestMod.idrnew file+5
@@ -0,0 +1,5 @@
1+module TestMod
2+
3+export
4+test : IO ()
5+test = putStrLn "Hello from a module"
test/interactive017/expectednew file+7
@@ -0,0 +1,7 @@
1+hello from C
2+hello from C
3+hello from node
4+hello from node
5+Hello ["aaa"]
6+Hello ["bbb", "aaa"]
7+Hello from a module
test/interactive017/runnew file+9
@@ -0,0 +1,9 @@
1+#!/bin/sh
2+PATH="../../scripts:$PATH"
3+./shebang.idr
4+./shebang.idr
5+./shebang-node.idr
6+./shebang-node.idr
7+./shebang-args.idr aaa
8+./shebang-args.idr bbb aaa
9+./shebang-import.idr
test/interactive017/shebang-args.idrnew file+6
@@ -0,0 +1,6 @@
1+#!/usr/bin/env runidris
2+
3+main : IO ()
4+main = do
5+ args <- getArgs
6+ putStrLn $ "Hello " ++ (show $ drop 1 args)
test/interactive017/shebang-import.idrnew file+6
@@ -0,0 +1,6 @@
1+#!/usr/bin/env runidris
2+
3+import TestMod
4+
5+main : IO ()
6+main = TestMod.test
test/interactive017/shebang-node.idrnew file+4
@@ -0,0 +1,4 @@
1+#!/usr/bin/env runidris-node
2+
3+main : IO ()
4+main = putStrLn "hello from node"
test/interactive017/shebang.idrnew file+4
@@ -0,0 +1,4 @@
1+#!/usr/bin/env runidris
2+
3+main : IO ()
4+main = putStrLn "hello from C"
test/pkg001/expected+3
@@ -18,3 +18,6 @@ builtin
1818Elaborating type decl Main.main[]
1919Elaborating clause Main.main
2020Rechecking for positivity []
21+The presented iPKG file does not have a '.ipkg' extension: "malformed-package-name"
22+The presented iPKG file does not exist: "non-existent-package.ipkg"
23+The presented iPKG file does not have a '.ipkg' extension: "non-existent-package-with-malformed-name"
test/pkg001/run+3
@@ -3,3 +3,6 @@ ${IDRIS:-idris} $@ --build test-pkg.ipkg
33rm -f *.ibc
44${IDRIS:-idris} $@ --build test-pkg.ipkg --quiet
55${IDRIS:-idris} $@ --build test-pkg.ipkg --logging-categories "elab" --log 1
6+${IDRIS:-idris} $@ --build malformed-package-name
7+${IDRIS:-idris} $@ --build non-existent-package.ipkg
8+${IDRIS:-idris} $@ --build non-existent-package-with-malformed-name
test/proof002/Reflect.idr+1−1
@@ -10,7 +10,7 @@ using (xs : List a, ys : List a, G : List (List a))
1010
1111 data Elem : a -> List a -> Type where
1212 Stop : Elem x (x :: xs)
13− Pop : Elem x ys -> Elem x (y :: xs)
13+ Pop : Elem x ys -> Elem x (y :: ys)
1414
1515-- Expr is a reflection of a list, indexed over the concrete list,
1616-- and over a set of list variables.
test/regression002/expected+2−1
@@ -110,7 +110,8 @@ reg068.idr:1:6:Main.nat has a name which may be implicitly bound.
110110This is likely to lead to problems!
111111reg068.idr:2:6:Main.ze has a name which may be implicitly bound.
112112This is likely to lead to problems!
113−reg068.idr:2:8-11:WARNING: nat is bound as an implicit
113+reg068.idr:2:8-11:
114+nat is bound as an implicit
114115 Did you mean to refer to Main.nat?
115116reg068.idr:2:6:When checking constructor Main.ze:
116117Type level variable nat is not Main.nat
test/regression003/expectednew file+1
@@ -0,0 +1 @@
1+ola
test/regression003/regression003.idrnew file+56
@@ -0,0 +1,56 @@
1+module Main
2+
3+data Free : (f : Type -> Type) -> (a : Type) -> Type where
4+ Pure : a -> Free f a
5+ Bind : f (Free f a) -> Free f a
6+
7+Functor f => Functor (Free f) where
8+ map f m = assert_total $ case m of
9+ Pure x => Pure (f x)
10+ Bind x => Bind (map (map f) x)
11+
12+Functor f => Applicative (Free f) where
13+ pure = Pure
14+
15+ m <*> x = assert_total $ case m of
16+ Pure f => map f x
17+ Bind f => Bind (map (<*> x) f)
18+
19+Functor f => Monad (Free f) where
20+ m >>= f = assert_total $ case m of
21+ Pure x => f x
22+ Bind x => Bind (map (>>= f) x)
23+
24+liftFree : Functor f => f a -> Free f a
25+liftFree = assert_total $ Bind . map Pure
26+
27+foldFree : (Monad m, Functor f) => ({ a : Type } -> f a -> m a) -> Free f b -> m b
28+foldFree f m = assert_total $ case m of
29+ Pure x => pure x
30+ Bind x => f x >>= foldFree f
31+
32+data FileSystemF next
33+ = ReadFile (String -> next)
34+
35+FileSystem : Type -> Type
36+FileSystem = Free FileSystemF
37+
38+Functor FileSystemF where
39+ map f (ReadFile nextFn) = ReadFile (f . nextFn)
40+
41+readFileF : FileSystem String
42+readFileF = liftFree $ ReadFile id
43+
44+
45+
46+interpret2 : FileSystemF a -> IO a
47+interpret2 (ReadFile nextFn) = do
48+ contents <- pure "ola"
49+ pure (nextFn contents)
50+
51+main : IO ()
52+main =
53+ do
54+ c <- foldFree interpret2 readFileF
55+ putStrLn' c
56+
test/regression003/runnew file+4
@@ -0,0 +1,4 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ regression003.idr -o regression003
3+./regression003
4+rm -f regression003 *.ibc