on master help sign in
Merge branch 'master' of Idris-dev into issue3796
ab65a30Edmund Smith
.travis.yml+4−14
@@ -1,3 +1,4 @@
1+dist: trusty
1sudo: false
2sudo: false
2
3
3language: c
4language: c
@@ -10,15 +11,6 @@ matrix:
10 include:
11 include:
11 - env: CABALVER="1.24" GHCVER="8.0.1" STACKVER="7.14" STYLISH=YES
12 - env: CABALVER="1.24" GHCVER="8.0.1" STACKVER="7.14" STYLISH=YES
12 addons: {apt: {packages: [cabal-install-1.24,ghc-8.0.1,hscolour], sources: [hvr-ghc]}}
13 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]}}
22 - env: CABALVER="1.22" GHCVER="7.10.3" TESTS="lib_doc doc"
14 - env: CABALVER="1.22" GHCVER="7.10.3" TESTS="lib_doc doc"
23 compiler: ": #GHC 7.10.3"
15 compiler: ": #GHC 7.10.3"
24 addons: {apt: {packages: [cabal-install-1.22,ghc-7.10.3,cppcheck,hscolour], sources: [hvr-ghc]}}
16 addons: {apt: {packages: [cabal-install-1.22,ghc-7.10.3,cppcheck,hscolour], sources: [hvr-ghc]}}
@@ -37,10 +29,6 @@ matrix:
37 - env: CABALVER="1.24" GHCVER="8.0.1" TESTS="test_c"
29 - env: CABALVER="1.24" GHCVER="8.0.1" TESTS="test_c"
38 compiler: ": #GHC 8.0.1"
30 compiler: ": #GHC 8.0.1"
39 addons: {apt: {packages: [cabal-install-1.24,ghc-8.0.1,cppcheck,hscolour], sources: [hvr-ghc]}}
31 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"
44 fast-finish: true
32 fast-finish: true
45
33
46cache:
34cache:
@@ -153,7 +141,9 @@ script:
153 - echo -en 'travis_fold:end:script.tests\\r'
141 - echo -en 'travis_fold:end:script.tests\\r'
154###
142###
155 - echo 'Benchmarks...' && echo -en 'travis_fold:start:script.benchmarks\\r'
143 - echo 'Benchmarks...' && echo -en 'travis_fold:start:script.benchmarks\\r'
144+ - if [[ "$TESTS" == "test_c" ]]; then
156− - cd benchmarks && ./build.pl && ./run.pl && cd ..
145+ cd benchmarks && ./build.pl && ./run.pl && cd ..;
146+ fi
157 - echo -en 'travis_fold:end:script.benchmarks\\r'
147 - echo -en 'travis_fold:end:script.benchmarks\\r'
158###
148###
159# EOF
149# 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`.
1
31
2## Tool Updates
32## Tool Updates
3
33
4+ New JavaScript code generator that uses an higher level intermediate
34+ New JavaScript code generator that uses an higher level intermediate
5 representation.
35 representation.
6
36
7−+ Various optimizations of the novel JavaScript code generator to make
37++ Various optimizations of the new JavaScript code generator.
8− its results fast.
9
38
10+ Names are now annotated with their representations over the IDE
39+ Names are now annotated with their representations over the IDE
11 protocol, which allows IDEs to provide commands that work on special
40 protocol, which allows IDEs to provide commands that work on special
README.md+1−1
@@ -3,7 +3,7 @@
3[![Build Status](https://travis-ci.org/idris-lang/Idris-dev.svg?branch=master)](https://travis-ci.org/idris-lang/Idris-dev)
3[![Build Status](https://travis-ci.org/idris-lang/Idris-dev.svg?branch=master)](https://travis-ci.org/idris-lang/Idris-dev)
4[![Appveyor build](https://ci.appveyor.com/api/projects/status/xi8yu81oy1134g7o/branch/master?svg=true)](https://ci.appveyor.com/project/idrislang/idris-dev)
4[![Appveyor build](https://ci.appveyor.com/api/projects/status/xi8yu81oy1134g7o/branch/master?svg=true)](https://ci.appveyor.com/project/idrislang/idris-dev)
5[![Documentation Status](https://readthedocs.org/projects/idris/badge/?version=latest)](https://readthedocs.org/projects/idris/?badge=latest)
5[![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)
7[![Stackage LTS](http://stackage.org/package/idris/badge/lts)](http://stackage.org/lts/package/idris)
7[![Stackage LTS](http://stackage.org/package/idris/badge/lts)](http://stackage.org/lts/package/idris)
8[![Stackage Nightly](http://stackage.org/package/idris/badge/nightly)](http://stackage.org/nightly/package/idris)
8[![Stackage Nightly](http://stackage.org/package/idris/badge/nightly)](http://stackage.org/nightly/package/idris)
9[![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)
9[![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)) $
274-- -----------------------------------------------------------------------------
274-- -----------------------------------------------------------------------------
275-- Test
275-- Test
276
276
277−-- FIXME: We use the __GLASGOW_HASKELL__ macro because MIN_VERSION_cabal seems
278−-- to be broken !
279−
280-- There are two "dataDir" in cabal, and they don't relate to each other.
277-- There are two "dataDir" in cabal, and they don't relate to each other.
281-- When fetching modules, idris uses the second path (in the pkg record),
278-- When fetching modules, idris uses the second path (in the pkg record),
282-- which by default is the root folder of the project.
279-- which by default is the root folder of the project.
283-- We want it to be the install directory where we put the idris libraries.
280-- We want it to be the install directory where we put the idris libraries.
284fixPkg pkg target = pkg { dataDir = target }
281fixPkg pkg target = pkg { dataDir = target }
285
282
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−
294idrisTestHook args pkg local hooks flags = do
283idrisTestHook args pkg local hooks flags = do
295 let target = datadir $ L.absoluteInstallDirs pkg local NoCopyDest
284 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
297
286
298-- -----------------------------------------------------------------------------
287-- -----------------------------------------------------------------------------
299-- Main
288-- Main
@@ -314,9 +303,5 @@ main = defaultMainWithHooks $ simpleUserHooks
314 , preSDist = idrisPreSDist
303 , preSDist = idrisPreSDist
315 , sDistHook = idrisSDist (sDistHook simpleUserHooks)
304 , sDistHook = idrisSDist (sDistHook simpleUserHooks)
316 , postSDist = idrisPostSDist
305 , postSDist = idrisPostSDist
317−#if __GLASGOW_HASKELL__ < 710
318− , testHook = idrisTestHook ()
319−#else
320 , testHook = idrisTestHook
306 , testHook = idrisTestHook
321−#endif
322 }
307 }
appveyor.yml+1−1
@@ -1,7 +1,7 @@
1version: 1.0.{build}
1version: 1.0.{build}
2init:
2init:
3- ps: >-
3- ps: >-
4− choco install cabal
4+ choco install cabal --no-progress
5
5
6 mkdir C:\ghc
6 mkdir C:\ghc
7
7
codegen/idris-codegen-c/Main.hs+1
@@ -4,6 +4,7 @@ import Idris.AbsSyntax
4import Idris.Core.TT
4import Idris.Core.TT
5import Idris.ElabDecls
5import Idris.ElabDecls
6import Idris.Main
6import Idris.Main
7+import Idris.Options
7import IRTS.CodegenC
8import IRTS.CodegenC
8import IRTS.Compiler
9import IRTS.Compiler
9
10
codegen/idris-codegen-javascript/Main.hs+1
@@ -4,6 +4,7 @@ import Idris.AbsSyntax
4import Idris.Core.TT
4import Idris.Core.TT
5import Idris.ElabDecls
5import Idris.ElabDecls
6import Idris.Main
6import Idris.Main
7+import Idris.Options
7import IRTS.CodegenJavaScript
8import IRTS.CodegenJavaScript
8import IRTS.Compiler
9import IRTS.Compiler
9
10
codegen/idris-codegen-node/Main.hs+1
@@ -4,6 +4,7 @@ import Idris.AbsSyntax
4import Idris.Core.TT
4import Idris.Core.TT
5import Idris.ElabDecls
5import Idris.ElabDecls
6import Idris.Main
6import Idris.Main
7+import Idris.Options
7import IRTS.CodegenJavaScript
8import IRTS.CodegenJavaScript
8import IRTS.Compiler
9import IRTS.Compiler
9
10
docs/reference/codegen.rst+10−10
@@ -27,16 +27,6 @@ issue the following command:
27 $ idris --codegen javascript hello.idr -o hello.js
27 $ idris --codegen javascript hello.idr -o hello.js
28
28
29
29
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−
40Idris can produce very big chunks of JavaScript code (hello world
30Idris can produce very big chunks of JavaScript code (hello world
41weighs in at 1500 lines). However, the generated code can be minified
31weighs in at 1500 lines). However, the generated code can be minified
42using the `closure-compiler
32using the `closure-compiler
@@ -50,6 +40,16 @@ using the `closure-compiler
50Node.js
40Node.js
51-------
41-------
52
42
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+
53
53
54Third Party
54Third Party
55============
55============
docs/reference/elaborator-reflection.rst+6−1
@@ -32,6 +32,9 @@ Running Elaborator Scripts
32
32
33On their own, tactics have no effect.
33On their own, tactics have no effect.
34The meta-operation ``%runElab script`` runs ``script`` in the current elaboration context.
34The 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).
35For example, the following script constructs the identity function at type ``Nat``:
38For example, the following script constructs the identity function at type ``Nat``:
36
39
37.. code-block:: idris
40.. code-block:: idris
@@ -88,7 +91,9 @@ that fills the hole.
88
91
89The interactive elaboration shell accepts a limited number of commands,
92The interactive elaboration shell accepts a limited number of commands,
90including a subset of the commands understood by the normal Idris REPL
93including 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``.
92
97
93General-purpose commands:
98General-purpose commands:
94
99
docs/reference/ide-protocol.rst+10−10
@@ -45,15 +45,12 @@ This is achieved by the already seen ``:load-file`` command.
45
45
46The available commands include:
46The available commands include:
47
47
48− ``(:load-file FILENAME)``
48+ ``(:load-file FILENAME [LINE])``
49− Load the named file.
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.
50
50
51 ``(:interpret STRING)``
51 ``(:interpret STRING)``
52 Interpret ``STRING`` at the Idris REPL, returning a highlighted result.
52 Interpret ``STRING`` at the Idris REPL, returning a highlighted result.
53
53
54− ``(:repl-completions STRING)``
55− Return the result of tab-completing ``STRING`` as a REPL command.
56−
57 ``(:type-of STRING)``
54 ``(:type-of STRING)``
58 Return the type of the name, written with Idris syntax in the ``STRING``.
55 Return the type of the name, written with Idris syntax in the ``STRING``.
59 The reply may contain highlighting information.
56 The reply may contain highlighting information.
@@ -88,9 +85,12 @@ The available commands include:
88 Attempt to fill out the holes on ``LINE`` named ``NAME`` by proof search.
85 Attempt to fill out the holes on ``LINE`` named ``NAME`` by proof search.
89 ``HINTS`` is a possibly-empty list of additional things to try while searching.
86 ``HINTS`` is a possibly-empty list of additional things to try while searching.
90
87
91− ``(:docs-for NAME)``
88+ ``(:docs-for NAME [MODE])``
92− Look up the documentation for ``NAME``, and return it as a highlighted string.
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``.
93−
90+
91+ ``(:apropos STRING)``
92+ Search the documentation for mentions of ``STRING``, and return any found as a list of highlighted strings.
93+
94 ``(:metavariables WIDTH)``
94 ``(:metavariables WIDTH)``
95 List the currently-active holes, with their types pretty-printed with ``WIDTH`` columns.
95 List the currently-active holes, with their types pretty-printed with ``WIDTH`` columns.
96
96
@@ -119,9 +119,9 @@ The available commands include:
119 Return the definition of ``NAME`` as a highlighted string.
119 Return the definition of ``NAME`` as a highlighted string.
120
120
121 ``(:repl-completions NAME)``
121 ``(: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.
123
123
124− ``(:version UID)``
124+ ``:version``
125 Return the version information of the Idris compiler.
125 Return the version information of the Idris compiler.
126
126
127
127
docs/reference/syntax-guide.rst+8−2
@@ -223,7 +223,7 @@ Every occurence of the the defined type in a constructor argument will be
223wrapped in the ``Inf`` type constructor. This has the effect of delaying the
223wrapped in the ``Inf`` type constructor. This has the effect of delaying the
224evaluation of the second argument when the data constructor is applied.
224evaluation of the second argument when the data constructor is applied.
225An ``Inf`` argument is constructed using ``Delay`` (which Idris will insert
225An ``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).
227
227
228Furthermore, recursive calls under a ``Delay`` must be guarded by a constructor
228Furthermore, recursive calls under a ``Delay`` must be guarded by a constructor
229to pass the totality checker.
229to pass the totality checker.
@@ -387,10 +387,16 @@ Totality
387::
387::
388
388
389 total
389 total
390− implicit
391 partial
390 partial
392 covering
391 covering
393
392
393+Implicit Coercion
394+^^^^^^^^^^^^^^^^^
395+
396+::
397+
398+ implicit
399+
394Options
400Options
395^^^^^^^
401^^^^^^^
396
402
docs/st/composing.rst+1−1
@@ -437,7 +437,7 @@ using the SDL bindings as follows:
437
437
438.. code-block:: idris
438.. code-block:: idris
439
439
440− interface Draw IO where
440+ implementation Draw IO where
441 Surface = State SDLSurface
441 Surface = State SDLSurface
442
442
443 initWindow x y = do Just srf <- lift (startSDL x y)
443 initWindow x y = do Just srf <- lift (startSDL x y)
docs/tutorial/interfaces.rst+2−2
@@ -48,8 +48,8 @@ For example, the
48Only one implementation of an interface can be given for a type — implementations may
48Only one implementation of an interface can be given for a type — implementations may
49not overlap. Implementation declarations can themselves have constraints.
49not overlap. Implementation declarations can themselves have constraints.
50To help with resolution, the arguments of an implementation must be
50To help with resolution, the arguments of an implementation must be
51−constructors (either data or type constructors), variables or
51+constructors (either data or type constructors) or variables
52−constants (i.e. you cannot give an implementation for a function). For
52+(i.e. you cannot give an implementation for a function). For
53example, to define a ``Show`` implementation for vectors, we need to know
53example, to define a ``Show`` implementation for vectors, we need to know
54that there is a ``Show`` implementation for the element type, because we are
54that there is a ``Show`` implementation for the element type, because we are
55going to use it to convert each element to a ``String``:
55going 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:
494 %include JavaScript "path/to/external.js"
494 %include JavaScript "path/to/external.js"
495
495
496The given files will be added to the top of the generated code.
496The 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.
497
506
498Including *NodeJS* modules
507Including *NodeJS* modules
499--------------------------
508--------------------------
idris.cabal+16−38
@@ -1,5 +1,5 @@
1Name: idris
1Name: idris
2−Version: 1.0
2+Version: 1.1.0
3License: BSD3
3License: BSD3
4License-file: LICENSE
4License-file: LICENSE
5Author: Edwin Brady
5Author: Edwin Brady
@@ -40,11 +40,11 @@ Description: Idris is a general purpose language with full dependent types.
40 .
40 .
41 * Hugs style interactive environment
41 * Hugs style interactive environment
42
42
43−Cabal-Version: >= 1.8.1
43+Cabal-Version: >= 1.18
44
44
45Build-type: Custom
45Build-type: Custom
46
46
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
48
48
49Data-files: idrisdoc/styles.css
49Data-files: idrisdoc/styles.css
50 jsrts/jsbn/jsbn-browser.js
50 jsrts/jsbn/jsbn-browser.js
@@ -196,6 +196,7 @@ Library
196 , Idris.Output
196 , Idris.Output
197 , Idris.Main
197 , Idris.Main
198 , Idris.ModeCommon
198 , Idris.ModeCommon
199+ , Idris.Options
199 , Idris.Parser
200 , Idris.Parser
200 , Idris.Parser.Helpers
201 , Idris.Parser.Helpers
201 , Idris.Parser.Ops
202 , Idris.Parser.Ops
@@ -258,7 +259,7 @@ Library
258 , Tools_idris
259 , Tools_idris
259
260
260 Build-depends: base >=4 && <5
261 Build-depends: base >=4 && <5
261− , aeson >= 0.6 && < 1.2
262+ , aeson >= 0.6 && < 1.3
262 , annotated-wl-pprint >= 0.7 && < 0.8
263 , annotated-wl-pprint >= 0.7 && < 0.8
263 , ansi-terminal < 0.7
264 , ansi-terminal < 0.7
264 , ansi-wl-pprint < 0.7
265 , ansi-wl-pprint < 0.7
@@ -276,20 +277,22 @@ Library
276 , filepath < 1.5
277 , filepath < 1.5
277 , fingertree >= 0.1 && < 0.2
278 , fingertree >= 0.1 && < 0.2
278 , haskeline >= 0.7 && < 0.8
279 , haskeline >= 0.7 && < 0.8
279− , ieee754 >= 0.7 && <= 0.8.0
280+ , ieee754 >= 0.7 && < 0.9
280 , mtl >= 2.1 && < 2.3
281 , mtl >= 2.1 && < 2.3
281 , network < 2.7
282 , network < 2.7
282− , optparse-applicative >= 0.11 && < 0.14
283+ , optparse-applicative >= 0.13 && < 0.15
283 , parsers >= 0.9 && < 0.13
284 , parsers >= 0.9 && < 0.13
284 , pretty < 1.2
285 , pretty < 1.2
286+ , process < 1.7
285 , regex-tdfa >= 1.2
287 , regex-tdfa >= 1.2
288+ , safe >= 0.3.9
286 , split < 0.3
289 , split < 0.3
287 , terminal-size < 0.4
290 , terminal-size < 0.4
288 , text >=1.2.1.0 && < 1.3
291 , text >=1.2.1.0 && < 1.3
289− , time >= 1.4 && < 1.7
292+ , time >= 1.4 && < 1.9
290 , transformers < 0.6
293 , transformers < 0.6
291 , transformers-compat >= 0.3
294 , transformers-compat >= 0.3
292− , trifecta >= 1.6 && < 1.7
295+ , trifecta >= 1.6 && < 1.8
293 , uniplate >=1.6 && < 1.7
296 , uniplate >=1.6 && < 1.7
294 , unordered-containers < 0.3
297 , unordered-containers < 0.3
295 , utf8-string < 1.1
298 , utf8-string < 1.1
@@ -299,34 +302,6 @@ Library
299 , fsnotify >= 0.2 && < 2.2
302 , fsnotify >= 0.2 && < 2.2
300 , async < 2.2
303 , async < 2.2
301
304
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−
330 ghc-prof-options: -auto-all -caf-all
305 ghc-prof-options: -auto-all -caf-all
331
306
332 if os(linux)
307 if os(linux)
@@ -364,6 +339,7 @@ Executable idris
364 , haskeline >= 0.7
339 , haskeline >= 0.7
365 , transformers
340 , transformers
366
341
342+ Default-Language: Haskell2010
367 ghc-prof-options: -auto-all -caf-all
343 ghc-prof-options: -auto-all -caf-all
368 ghc-options: -threaded -rtsopts -funbox-strict-fields -with-rtsopts=-I0
344 ghc-options: -threaded -rtsopts -funbox-strict-fields -with-rtsopts=-I0
369
345
@@ -388,10 +364,9 @@ Test-suite regression-and-feature-tests
388 , tasty-rerun >= 1.0.0
364 , tasty-rerun >= 1.0.0
389 , bytestring
365 , bytestring
390 , transformers
366 , transformers
391− if impl(ghc < 7.10)
392− Extensions: DeriveDataTypeable
393
367
394
368
369+ Default-Language: Haskell2010
395 ghc-prof-options: -auto-all -caf-all
370 ghc-prof-options: -auto-all -caf-all
396 ghc-options: -threaded -rtsopts -with-rtsopts=-N -funbox-strict-fields
371 ghc-options: -threaded -rtsopts -with-rtsopts=-N -funbox-strict-fields
397
372
@@ -405,6 +380,7 @@ Executable idris-codegen-c
405 , haskeline >= 0.7
380 , haskeline >= 0.7
406 , transformers
381 , transformers
407
382
383+ Default-Language: Haskell2010
408 ghc-prof-options: -auto-all -caf-all
384 ghc-prof-options: -auto-all -caf-all
409 ghc-options: -threaded -rtsopts -funbox-strict-fields
385 ghc-options: -threaded -rtsopts -funbox-strict-fields
410
386
@@ -418,6 +394,7 @@ Executable idris-codegen-javascript
418 , haskeline >= 0.7
394 , haskeline >= 0.7
419 , transformers
395 , transformers
420
396
397+ Default-Language: Haskell2010
421 ghc-prof-options: -auto-all -caf-all
398 ghc-prof-options: -auto-all -caf-all
422 ghc-options: -threaded -rtsopts -funbox-strict-fields
399 ghc-options: -threaded -rtsopts -funbox-strict-fields
423
400
@@ -431,5 +408,6 @@ Executable idris-codegen-node
431 , haskeline >= 0.7
408 , haskeline >= 0.7
432 , transformers
409 , transformers
433
410
411+ Default-Language: Haskell2010
434 ghc-prof-options: -auto-all -caf-all
412 ghc-prof-options: -auto-all -caf-all
435 ghc-options: -threaded -rtsopts -funbox-strict-fields
413 ghc-options: -threaded -rtsopts -funbox-strict-fields
libs/base/Control/Catchable.idr+22
@@ -1,6 +1,10 @@
1module Control.Catchable
1module Control.Catchable
2
2
3import Control.IOExcept
3import Control.IOExcept
4+import Control.Monad.Reader
5+import Control.Monad.Writer
6+import Control.Monad.RWS
7+import Control.Monad.Trans
4
8
5%access public export
9%access public export
6
10
@@ -32,3 +36,21 @@ implementation Catchable List () where
32 catch xs h = xs
36 catch xs h = xs
33
37
34 throw () = []
38 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
14record RWST (r : Type) (w : Type) (s : Type) (m : Type -> Type) (a : Type) where
14record RWST (r : Type) (w : Type) (s : Type) (m : Type -> Type) (a : Type) where
15 constructor MkRWST
15 constructor MkRWST
16 runRWST : r -> s -> m (a, s, w)
16 runRWST : r -> s -> m (a, s, w)
17−
17+
18implementation Monad m => Functor (RWST r w s m) where
18implementation Monad m => Functor (RWST r w s m) where
19 map f (MkRWST m) = MkRWST $ \r,s => do (a, s', w) <- m r s
19 map f (MkRWST m) = MkRWST $ \r,s => do (a, s', w) <- m r s
20 pure (f a, s', w)
20 pure (f a, s', w)
@@ -48,6 +48,12 @@ implementation (Monoid w, Monad m) => MonadState s (RWST r w s m) where
48
48
49implementation (Monoid w, Monad m) => MonadRWS r w s (RWST r w s m) where {}
49implementation (Monoid w, Monad m) => MonadRWS r w s (RWST r w s m) where {}
50
50
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+
51||| The RWS monad. See the MonadRWS interface
57||| The RWS monad. See the MonadRWS interface
52RWS : Type -> Type -> Type -> Type -> Type
58RWS : Type -> Type -> Type -> Type -> Type
53RWS r w s a = RWST r w s Identity a
59RWS 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
61 (lrec : Lazy (SplitRec lefts)) ->
61 (lrec : Lazy (SplitRec lefts)) ->
62 (rrec : Lazy (SplitRec rights)) -> SplitRec (lefts ++ rights)
62 (rrec : Lazy (SplitRec rights)) -> SplitRec (lefts ++ rights)
63
63
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−
75||| Covering function for the `SplitRec` view
64||| Covering function for the `SplitRec` view
76||| Constructs the view in O(n lg n)
65||| Constructs the view in O(n lg n)
77−export total
66+public export total
78splitRec : (xs : List a) -> SplitRec xs
67splitRec : (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))
80
76
81||| View for traversing a list backwards
77||| View for traversing a list backwards
82public export
78public export
@@ -105,21 +101,21 @@ data Filtered : (a -> a -> Bool) -> List a -> Type where
105 (rrec : Lazy (Filtered p (filter (\y => not (p y x)) xs))) ->
101 (rrec : Lazy (Filtered p (filter (\y => not (p y x)) xs))) ->
106 Filtered p (x :: xs)
102 Filtered p (x :: xs)
107
103
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)
109filteredLOK p x xs = LTESucc (filterSmaller xs)
105filteredLOK p x xs = LTESucc (filterSmaller xs)
110
106
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)
112filteredROK p x xs = LTESucc (filterSmaller xs)
108filteredROK p x xs = LTESucc (filterSmaller xs)
113
109
114||| Covering function for the `Filtered` view
110||| Covering function for the `Filtered` view
115||| Constructs the view in O(n lg n)
111||| Constructs the view in O(n lg n)
116−export
112+public export total
117filtered : (p : a -> a -> Bool) -> (xs : List a) -> Filtered p xs
113filtered : (p : a -> a -> Bool) -> (xs : List a) -> Filtered p xs
118−filtered p inp with (smallerAcc inp)
114+filtered p inp with (sizeAccessible inp)
119− filtered p [] | with_pat = FNil
115+ filtered p [] | _ = FNil
120− filtered p (x :: xs) | (Access xsrec)
116+ filtered p (x :: xs) | Access acc
121− = FRec (filtered p (filter (\y => p y x) xs) | xsrec _ (filteredLOK p x xs))
117+ = FRec (filtered p (filter (\y => p y x) xs) | acc _ (filteredLOK p x xs))
122− (filtered p (filter (\y => not (p y x)) xs) | xsrec _ (filteredROK p x xs))
118+ (filtered p (filter (\y => not (p y x)) xs) | acc _ (filteredROK p x xs))
123
119
124lenImpossible : (n = Z) -> (n = ((S k) + right)) -> Void
120lenImpossible : (n = Z) -> (n = ((S k) + right)) -> Void
125lenImpossible {n = Z} _ Refl impossible
121lenImpossible {n = Z} _ Refl impossible
libs/base/Data/Nat/Views.idr+9−13
@@ -22,17 +22,13 @@ half (S k) with (half k)
22 HalfEven {n=S n}
22 HalfEven {n=S n}
23 half (S (n + n)) | HalfEven = HalfOdd
23 half (S (n + n)) | HalfEven = HalfOdd
24
24
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
36halfRec : (n : Nat) -> HalfRec n
26halfRec : (n : Nat) -> HalfRec n
37−halfRec n = accInd halfRecFix n (ltAccessible n)
27+halfRec n with (sizeAccessible n)
38−
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
61 (lrec : Lazy (SplitRec xs)) ->
61 (lrec : Lazy (SplitRec xs)) ->
62 (rrec : Lazy (SplitRec ys)) -> SplitRec (xs ++ ys)
62 (rrec : Lazy (SplitRec ys)) -> SplitRec (xs ++ ys)
63
63
64−smallerPlus : LTE (S (S m)) (S (plus m (S k)))
64+smallerPlusL : LTE (S (S m)) (S (plus m (S k)))
65−smallerPlus {m} {k} = rewrite sym (plusSuccRightSucc m k) in
65+smallerPlusL {m} {k} = rewrite sym (plusSuccRightSucc m k) in
66 (LTESucc (LTESucc (lteAddRight _)))
66 (LTESucc (LTESucc (lteAddRight _)))
67
67
68−smallerPlus' : LTE (S (S k)) (S (plus m (S k)))
68+smallerPlusR : LTE (S (S k)) (S (plus m (S k)))
69−smallerPlus' {m} {k} = rewrite sym (plusSuccRightSucc m k) in
69+smallerPlusR {m} {k} = rewrite sym (plusSuccRightSucc m k) in
70 LTESucc (LTESucc (rewrite plusCommutative m k in (lteAddRight _)))
70 LTESucc (LTESucc (rewrite plusCommutative m k in (lteAddRight _)))
71
71
72||| Covering function for the `SplitRec` view
72||| Covering function for the `SplitRec` view
73||| Constructs the view in O(n lg n)
73||| Constructs the view in O(n lg n)
74−export
74+public export total
75splitRec : (xs : Vect n a) -> SplitRec xs
75splitRec : (xs : Vect n a) -> SplitRec xs
76−splitRec {n} input with (ltAccessible n)
76+splitRec {n} input with (sizeAccessible n)
77 splitRec input | acc with (split input)
77 splitRec input | acc with (split input)
78 splitRec [] | acc | SplitNil = SplitRecNil
78 splitRec [] | acc | SplitNil = SplitRecNil
79 splitRec [x] | acc | SplitOne = SplitRecOne
79 splitRec [x] | acc | SplitOne = SplitRecOne
80− splitRec (x :: (xs ++ (y :: ys))) | (Access rec) | SplitPair
80+ splitRec (x :: (xs ++ (y :: ys))) | Access acc | SplitPair
81− = let left = splitRec (x :: xs) | rec _ smallerPlus
82− right = splitRec (y :: ys) | rec _ smallerPlus' in
83− SplitRecPair left right
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
132-- Properties
132-- Properties
133--------------------------------------------------------------------------------
133--------------------------------------------------------------------------------
134
134
135−total
136−absurdBoolDischarge : False = True -> Void
137−absurdBoolDischarge Refl impossible
138−
139total
135total
140isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = Z
136isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = Z
141isEmptySizeZero Empty p = Refl
137isEmptySizeZero Empty p = Refl
libs/contrib/Data/SortedMap.idr+52−1
@@ -1,6 +1,6 @@
1module Data.SortedMap
1module Data.SortedMap
2
2
3−-- TODO: write merge and split
3+-- TODO: write split
4
4
5private
5private
6data Tree : Nat -> (k : Type) -> Type -> Ord k -> Type where
6data Tree : Nat -> (k : Type) -> Type -> Ord k -> Type where
@@ -214,6 +214,10 @@ insert k v (M _ t) =
214 Left t' => (M _ t')
214 Left t' => (M _ t')
215 Right t' => (M _ t')
215 Right t' => (M _ t')
216
216
217+export
218+insertFrom : Foldable f => f (k, v) -> SortedMap k v -> SortedMap k v
219+insertFrom = flip $ foldl $ flip $ uncurry insert
220+
217export
221export
218delete : k -> SortedMap k v -> SortedMap k v
222delete : k -> SortedMap k v -> SortedMap k v
219delete _ Empty = Empty
223delete _ Empty = Empty
@@ -235,6 +239,16 @@ toList : SortedMap k v -> List (k, v)
235toList Empty = []
239toList Empty = []
236toList (M _ t) = treeToList t
240toList (M _ t) = treeToList t
237
241
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+
238treeMap : (a -> b) -> Tree n k a o -> Tree n k b o
252treeMap : (a -> b) -> Tree n k a o -> Tree n k b o
239treeMap f (Leaf k v) = Leaf k (f v)
253treeMap f (Leaf k v) = Leaf k (f v)
240treeMap f (Branch2 t1 k t2) = Branch2 (treeMap f t1) k (treeMap f t2)
254treeMap f (Branch2 t1 k t2) = Branch2 (treeMap f t1) k (treeMap f t2)
@@ -245,3 +259,40 @@ export
245implementation Functor (SortedMap k) where
259implementation Functor (SortedMap k) where
246 map _ Empty = Empty
260 map _ Empty = Empty
247 map f (M n t) = M _ (treeMap f t)
261 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
60export
60export
61Ord k => Monoid (SortedSet k) where
61Ord k => Monoid (SortedSet k) where
62 neutral = empty
62 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,
30
30
31 System.Concurrency.Process,
31 System.Concurrency.Process,
32
32
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+
33 Data.Fin.Extra
40 Data.Fin.Extra
libs/prelude/Decidable/Equality.idr+15−9
@@ -8,18 +8,10 @@ import Prelude.Either
8import Prelude.List
8import Prelude.List
9import Prelude.Nat
9import Prelude.Nat
10import Prelude.Maybe
10import Prelude.Maybe
11+import Prelude.Uninhabited
11
12
12%access public export
13%access public export
13
14
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−
23--------------------------------------------------------------------------------
15--------------------------------------------------------------------------------
24-- Decidable equality
16-- Decidable equality
25--------------------------------------------------------------------------------
17--------------------------------------------------------------------------------
@@ -29,6 +21,20 @@ interface DecEq t where
29 ||| Decide whether two elements of `t` are propositionally equal
21 ||| Decide whether two elements of `t` are propositionally equal
30 total decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
22 total decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
31
23
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+
32--------------------------------------------------------------------------------
38--------------------------------------------------------------------------------
33--- Unit
39--- Unit
34--------------------------------------------------------------------------------
40--------------------------------------------------------------------------------
libs/prelude/Prelude/Bool.idr+9
@@ -35,3 +35,12 @@ not : Bool -> Bool
35not True = False
35not True = False
36not False = True
36not False = True
37
37
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
7
7
8||| Interface for transforming an instance of a data type to another type.
8||| Interface for transforming an instance of a data type to another type.
9interface Cast from to where
9interface Cast from to where
10− ||| Perform a cast operation.
10+ ||| Perform a (potentially lossy!) cast operation.
11 |||
11 |||
12 ||| @orig The original type.
12 ||| @orig The original type.
13 cast : (orig : from) -> to
13 cast : (orig : from) -> to
libs/prelude/Prelude/Doubles.idr+3
@@ -21,6 +21,9 @@ exp x = prim__floatExp x
21log : Double -> Double
21log : Double -> Double
22log x = prim__floatLog x
22log x = prim__floatLog x
23
23
24+pow : Double -> Double -> Double
25+pow x y = exp (y * log x)
26+
24sin : Double -> Double
27sin : Double -> Double
25sin x = prim__floatSin x
28sin x = prim__floatSin x
26
29
libs/prelude/Prelude/List.idr+5−1
@@ -378,7 +378,7 @@ scanl : (b -> a -> b) -> b -> List a -> List b
378scanl f q [] = [q]
378scanl f q [] = [q]
379scanl f q (x::xs) = q :: scanl f (f q x) xs
379scanl f q (x::xs) = q :: scanl f (f q x) xs
380
380
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
382||| starting value.
382||| starting value.
383||| It assumes the first element of the list to be the starting value and then
383||| It assumes the first element of the list to be the starting value and then
384||| starts the fold with the element following it.
384||| starts the fold with the element following it.
@@ -855,6 +855,10 @@ catMaybes (x::xs) =
855-- Properties
855-- Properties
856--------------------------------------------------------------------------------
856--------------------------------------------------------------------------------
857
857
858+||| (::) is injective
859+consInjective : (x :: xs) = (y :: ys) -> (x = y, xs = ys)
860+consInjective Refl = (Refl, Refl)
861+
858||| The empty list is a right identity for append.
862||| The empty list is a right identity for append.
859appendNilRightNeutral : (l : List a) ->
863appendNilRightNeutral : (l : List a) ->
860 l ++ [] = l
864 l ++ [] = l
libs/prelude/Prelude/Monad.idr+6−1
@@ -6,6 +6,7 @@ import Builtins
6import Prelude.Functor
6import Prelude.Functor
7import public Prelude.Applicative
7import public Prelude.Applicative
8import Prelude.Basics
8import Prelude.Basics
9+import Prelude.Foldable
9import IO
10import IO
10
11
11%access public export
12%access public export
@@ -33,6 +34,11 @@ flatten : Monad m => m (m a) -> m a
33flatten = join
34flatten = join
34%deprecate flatten "Please use `join`, which is the standard name."
35%deprecate flatten "Please use `join`, which is the standard name."
35
36
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+
36-- Annoyingly, these need to be here, so that we can use them in other
42-- Annoyingly, these need to be here, so that we can use them in other
37-- Prelude modules other than the top level.
43-- Prelude modules other than the top level.
38
44
@@ -48,4 +54,3 @@ Applicative (IO' ffi) where
48
54
49Monad (IO' ffi) where
55Monad (IO' ffi) where
50 b >>= k = io_bind b k
56 b >>= k = io_bind b k
51−
libs/prelude/Prelude/Nat.idr+2−5
@@ -191,13 +191,10 @@ maximum Z m = m
191maximum (S n) Z = S n
191maximum (S n) Z = S n
192maximum (S n) (S m) = S (maximum n m)
192maximum (S n) (S m) = S (maximum n m)
193
193
194−||| Tail recursive cast Nat to Int
194+||| Cast Nat to Int
195||| Note that this can overflow
195||| Note that this can overflow
196toIntNat : Nat -> Int
196toIntNat : Nat -> Int
197−toIntNat n = toIntNat' n 0 where
197+toIntNat n = prim__truncBigInt_Int (toIntegerNat n)
198− toIntNat' : Nat -> Int -> Int
199− toIntNat' Z x = x
200− toIntNat' (S n) x = toIntNat' n (x + 1)
201
198
202(-) : (m : Nat) -> (n : Nat) -> {auto smaller : LTE n m} -> Nat
199(-) : (m : Nat) -> (n : Nat) -> {auto smaller : LTE n m} -> Nat
203(-) m n {smaller} = minus m n
200(-) m n {smaller} = minus m n
libs/prelude/Prelude/WellFounded.idr+40−22
@@ -85,28 +85,46 @@ wfInd : WellFounded rel => {P : a -> Type} ->
85 (x : a) -> P x
85 (x : a) -> P x
86wfInd {rel} step x = accInd step x (wellFounded {rel} x)
86wfInd {rel} step x = accInd step x (wellFounded {rel} x)
87
87
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
89
94
90−||| LT is a well-founded relation on numbers
95+Smaller : Sized a => a -> a -> Type
91−ltAccessible : (n : Nat) -> Accessible LT n
96+Smaller x y = size x `LT` size y
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))
111
97
98+SizeAccessible : Sized a => a -> Type
99+SizeAccessible = Accessible Smaller
112
100
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
11import Idris.Error
11import Idris.Error
12import Idris.Info.Show
12import Idris.Info.Show
13import Idris.Main
13import Idris.Main
14+import Idris.Options
14import Idris.Package
15import Idris.Package
15
16
16import Util.System (setupBundledCC)
17import Util.System (setupBundledCC)
rts/idris_gc.c+1−1
@@ -24,7 +24,7 @@ VAL copy(VM* vm, VAL x) {
24 cl = MKFLOATc(vm, x->info.f);
24 cl = MKFLOATc(vm, x->info.f);
25 break;
25 break;
26 case CT_STRING:
26 case CT_STRING:
27− cl = MKSTRc(vm, x->info.str);
27+ cl = MKSTRclen(vm, x->info.str.str, x->info.str.len);
28 break;
28 break;
29 case CT_STROFFSET:
29 case CT_STROFFSET:
30 cl = MKSTROFFc(vm, x->info.str_offset);
30 cl = MKSTROFFc(vm, x->info.str_offset);
rts/idris_gmp.h+2
@@ -7,6 +7,8 @@
7#include "mini-gmp.h"
7#include "mini-gmp.h"
8#endif
8#endif
9
9
10+#include "idris_rts.h"
11+
10// Set memory allocation functions
12// Set memory allocation functions
11void init_gmpalloc(void);
13void init_gmpalloc(void);
12
14
rts/idris_main.c+1
@@ -3,6 +3,7 @@
3#include "idris_rts.h"
3#include "idris_rts.h"
4#include "idris_stats.h"
4#include "idris_stats.h"
5
5
6+void _idris__123_runMain_95_0_125_(VM* vm, VAL* oldbase);
6#if defined(WIN32) || defined(__WIN32) || defined(__WIN32__)
7#if defined(WIN32) || defined(__WIN32) || defined(__WIN32__)
7#include <Windows.h>
8#include <Windows.h>
8int win32_get_argv_utf8(int *argc_ptr, char ***argv_ptr)
9int 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) {
285 Closure* cl = allocate(sizeof(Closure) + // Type) + sizeof(char*) +
285 Closure* cl = allocate(sizeof(Closure) + // Type) + sizeof(char*) +
286 sizeof(char)*len, 0);
286 sizeof(char)*len, 0);
287 SETTY(cl, CT_STRING);
287 SETTY(cl, CT_STRING);
288− cl -> info.str = (char*)cl + sizeof(Closure);
288+ cl->info.str.str = (char*)cl + sizeof(Closure);
289 if (str == NULL) {
289 if (str == NULL) {
290− cl->info.str = NULL;
290+ cl->info.str.str = NULL;
291 } else {
291 } else {
292− strcpy(cl -> info.str, str);
292+ strcpy(cl->info.str.str, str);
293 }
293 }
294+ cl->info.str.len = len > 0 ? len : 0;
294 return cl;
295 return cl;
295}
296}
296
297
297char* GETSTROFF(VAL stroff) {
298char* GETSTROFF(VAL stroff) {
298 // Assume STROFF
299 // Assume STROFF
299 StrOffset* root = stroff->info.str_offset;
300 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);
301}
309}
302
310
303VAL MKCDATA(VM* vm, CHeapItem * item) {
311VAL MKCDATA(VM* vm, CHeapItem * item) {
@@ -342,12 +350,26 @@ VAL MKFLOATc(VM* vm, double val) {
342}
350}
343
351
344VAL MKSTRc(VM* vm, char* str) {
352VAL 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) {
345 Closure* cl = allocate(sizeof(Closure) + // Type) + sizeof(char*) +
366 Closure* cl = allocate(sizeof(Closure) + // Type) + sizeof(char*) +
346− sizeof(char)*strlen(str)+1, 1);
367+ sizeof(char)*len+1, 1);
347 SETTY(cl, CT_STRING);
368 SETTY(cl, CT_STRING);
348− cl -> info.str = (char*)cl + sizeof(Closure);
369+ cl -> info.str.str = (char*)cl + sizeof(Closure);
349
370
350− strcpy(cl -> info.str, str);
371+ strcpy(cl->info.str.str, str);
372+ cl->info.str.len = len;
351 return cl;
373 return cl;
352}
374}
353
375
@@ -397,6 +419,13 @@ VAL MKB64(VM* vm, uint64_t bits64) {
397 return cl;
419 return cl;
398}
420}
399
421
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+
400void dumpStack(VM* vm) {
429void dumpStack(VM* vm) {
401 int i = 0;
430 int i = 0;
402 VAL* root;
431 VAL* root;
@@ -404,7 +433,8 @@ void dumpStack(VM* vm) {
404 for (root = vm->valstack; root < vm->valstack_top; ++root, ++i) {
433 for (root = vm->valstack; root < vm->valstack_top; ++root, ++i) {
405 printf("%d: ", i);
434 printf("%d: ", i);
406 dumpVal(*root);
435 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"); }
408 printf("\n");
438 printf("\n");
409 }
439 }
410 printf("RET: ");
440 printf("RET: ");
@@ -428,7 +458,7 @@ void dumpVal(VAL v) {
428 printf("] ");
458 printf("] ");
429 break;
459 break;
430 case CT_STRING:
460 case CT_STRING:
431− printf("STR[%s]", v->info.str);
461+ printf("STR[%s]", v->info.str.str);
432 break;
462 break;
433 case CT_FWD:
463 case CT_FWD:
434 printf("CT_FWD ");
464 printf("CT_FWD ");
@@ -490,8 +520,9 @@ VAL idris_castIntStr(VM* vm, VAL i) {
490 int x = (int) GETINT(i);
520 int x = (int) GETINT(i);
491 Closure* cl = allocate(sizeof(Closure) + sizeof(char)*16, 0);
521 Closure* cl = allocate(sizeof(Closure) + sizeof(char)*16, 0);
492 SETTY(cl, CT_STRING);
522 SETTY(cl, CT_STRING);
493− cl -> info.str = (char*)cl + sizeof(Closure);
523+ cl->info.str.str = (char*)cl + sizeof(Closure);
494− sprintf(cl -> info.str, "%d", x);
524+ sprintf(cl->info.str.str, "%d", x);
525+ cl->info.str.len = strlen(cl->info.str.str);
495 return cl;
526 return cl;
496}
527}
497
528
@@ -503,32 +534,33 @@ VAL idris_castBitsStr(VM* vm, VAL i) {
503 case CT_BITS8:
534 case CT_BITS8:
504 // max length 8 bit unsigned int str 3 chars (256)
535 // max length 8 bit unsigned int str 3 chars (256)
505 cl = allocate(sizeof(Closure) + sizeof(char)*4, 0);
536 cl = allocate(sizeof(Closure) + sizeof(char)*4, 0);
506− cl->info.str = (char*)cl + sizeof(Closure);
537+ cl->info.str.str = (char*)cl + sizeof(Closure);
507− sprintf(cl->info.str, "%" PRIu8, (uint8_t)i->info.bits8);
538+ sprintf(cl->info.str.str, "%" PRIu8, (uint8_t)i->info.bits8);
508 break;
539 break;
509 case CT_BITS16:
540 case CT_BITS16:
510 // max length 16 bit unsigned int str 5 chars (65,535)
541 // max length 16 bit unsigned int str 5 chars (65,535)
511 cl = allocate(sizeof(Closure) + sizeof(char)*6, 0);
542 cl = allocate(sizeof(Closure) + sizeof(char)*6, 0);
512− cl->info.str = (char*)cl + sizeof(Closure);
543+ cl->info.str.str = (char*)cl + sizeof(Closure);
513− sprintf(cl->info.str, "%" PRIu16, (uint16_t)i->info.bits16);
544+ sprintf(cl->info.str.str, "%" PRIu16, (uint16_t)i->info.bits16);
514 break;
545 break;
515 case CT_BITS32:
546 case CT_BITS32:
516 // max length 32 bit unsigned int str 10 chars (4,294,967,295)
547 // max length 32 bit unsigned int str 10 chars (4,294,967,295)
517 cl = allocate(sizeof(Closure) + sizeof(char)*11, 0);
548 cl = allocate(sizeof(Closure) + sizeof(char)*11, 0);
518− cl->info.str = (char*)cl + sizeof(Closure);
549+ cl->info.str.str = (char*)cl + sizeof(Closure);
519− sprintf(cl->info.str, "%" PRIu32, (uint32_t)i->info.bits32);
550+ sprintf(cl->info.str.str, "%" PRIu32, (uint32_t)i->info.bits32);
520 break;
551 break;
521 case CT_BITS64:
552 case CT_BITS64:
522 // max length 64 bit unsigned int str 20 chars (18,446,744,073,709,551,615)
553 // max length 64 bit unsigned int str 20 chars (18,446,744,073,709,551,615)
523 cl = allocate(sizeof(Closure) + sizeof(char)*21, 0);
554 cl = allocate(sizeof(Closure) + sizeof(char)*21, 0);
524− cl->info.str = (char*)cl + sizeof(Closure);
555+ cl->info.str.str = (char*)cl + sizeof(Closure);
525− sprintf(cl->info.str, "%" PRIu64, (uint64_t)i->info.bits64);
556+ sprintf(cl->info.str.str, "%" PRIu64, (uint64_t)i->info.bits64);
526 break;
557 break;
527 default:
558 default:
528 fprintf(stderr, "Fatal Error: ClosureType %d, not an integer type", ty);
559 fprintf(stderr, "Fatal Error: ClosureType %d, not an integer type", ty);
529 exit(EXIT_FAILURE);
560 exit(EXIT_FAILURE);
530 }
561 }
531
562
563+ cl->info.str.len = strlen(cl->info.str.str);
532 SETTY(cl, CT_STRING);
564 SETTY(cl, CT_STRING);
533 return cl;
565 return cl;
534}
566}
@@ -545,8 +577,10 @@ VAL idris_castStrInt(VM* vm, VAL i) {
545VAL idris_castFloatStr(VM* vm, VAL i) {
577VAL idris_castFloatStr(VM* vm, VAL i) {
546 Closure* cl = allocate(sizeof(Closure) + sizeof(char)*32, 0);
578 Closure* cl = allocate(sizeof(Closure) + sizeof(char)*32, 0);
547 SETTY(cl, CT_STRING);
579 SETTY(cl, CT_STRING);
548− cl -> info.str = (char*)cl + sizeof(Closure);
580+ cl->info.str.str = (char*)cl + sizeof(Closure);
549− snprintf(cl -> info.str, 32, "%.16g", GETFLOAT(i));
581+ snprintf(cl->info.str.str, 32, "%.16g", GETFLOAT(i));
582+
583+ cl->info.str.len = strlen(cl->info.str.str);
550 return cl;
584 return cl;
551}
585}
552
586
@@ -559,11 +593,13 @@ VAL idris_concat(VM* vm, VAL l, VAL r) {
559 char *ls = GETSTR(l);
593 char *ls = GETSTR(l);
560 // dumpVal(l);
594 // dumpVal(l);
561 // printf("\n");
595 // 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);
563 SETTY(cl, CT_STRING);
597 SETTY(cl, CT_STRING);
564− cl -> info.str = (char*)cl + sizeof(Closure);
598+ cl->info.str.str = (char*)cl + sizeof(Closure);
565− strcpy(cl -> info.str, ls);
599+ strcpy(cl->info.str.str, ls);
566− strcat(cl -> info.str, rs);
600+ strcat(cl->info.str.str, rs);
601+
602+ cl->info.str.len = GETSTRLEN(l) + GETSTRLEN(r);
567 return cl;
603 return cl;
568}
604}
569
605
@@ -670,21 +706,26 @@ VAL idris_strTail(VM* vm, VAL str) {
670VAL idris_strCons(VM* vm, VAL x, VAL xs) {
706VAL idris_strCons(VM* vm, VAL x, VAL xs) {
671 char *xstr = GETSTR(xs);
707 char *xstr = GETSTR(xs);
672 int xval = GETINT(x);
708 int xval = GETINT(x);
709+ int xlen = GETSTRLEN(xs);
710+
673 if ((xval & 0x80) == 0) { // ASCII char
711 if ((xval & 0x80) == 0) { // ASCII char
674 Closure* cl = allocate(sizeof(Closure) +
712 Closure* cl = allocate(sizeof(Closure) +
675− strlen(xstr) + 2, 0);
713+ xlen + 2, 0);
676 SETTY(cl, CT_STRING);
714 SETTY(cl, CT_STRING);
677− cl -> info.str = (char*)cl + sizeof(Closure);
715+ cl->info.str.str = (char*)cl + sizeof(Closure);
678− cl -> info.str[0] = (char)(GETINT(x));
716+ cl->info.str.str[0] = (char)(GETINT(x));
679− strcpy(cl -> info.str+1, xstr);
717+ strcpy(cl->info.str.str+1, xstr);
718+ cl->info.str.len = xlen + 1;
680 return cl;
719 return cl;
681 } else {
720 } else {
682 char *init = idris_utf8_fromChar(xval);
721 char *init = idris_utf8_fromChar(xval);
722+ int newlen = strlen(init) + xlen;
683− Closure* cl = allocate(sizeof(Closure) + strlen(init) + strlen(xstr) + 1, 0);
723+ Closure* cl = allocate(sizeof(Closure) + newlen + 1, 0);
684 SETTY(cl, CT_STRING);
724 SETTY(cl, CT_STRING);
685− cl -> info.str = (char*)cl + sizeof(Closure);
725+ cl->info.str.str = (char*)cl + sizeof(Closure);
686− strcpy(cl -> info.str, init);
726+ strcpy(cl->info.str.str, init);
687− strcat(cl -> info.str, xstr);
727+ strcat(cl->info.str.str, xstr);
728+ cl->info.str.len = newlen;
688 free(init);
729 free(init);
689 return cl;
730 return cl;
690 }
731 }
@@ -701,7 +742,7 @@ VAL idris_substr(VM* vm, VAL offset, VAL length, VAL str) {
701 char* str_val = GETSTR(str);
742 char* str_val = GETSTR(str);
702
743
703 // If the substring is a suffix, use idris_strShift to avoid reallocating
744 // 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)) {
705 return idris_strShift(vm, str, offset_val);
746 return idris_strShift(vm, str, offset_val);
706 }
747 }
707 else {
748 else {
@@ -709,20 +750,23 @@ VAL idris_substr(VM* vm, VAL offset, VAL length, VAL str) {
709 char *end = idris_utf8_advance(start, length_val);
750 char *end = idris_utf8_advance(start, length_val);
710 Closure* newstr = allocate(sizeof(Closure) + (end - start) +1, 0);
751 Closure* newstr = allocate(sizeof(Closure) + (end - start) +1, 0);
711 SETTY(newstr, CT_STRING);
752 SETTY(newstr, CT_STRING);
712− newstr -> info.str = (char*)newstr + sizeof(Closure);
753+ newstr->info.str.str = (char*)newstr + sizeof(Closure);
713− memcpy(newstr -> info.str, start, end - start);
754+ memcpy(newstr->info.str.str, start, end - start);
714− *(newstr -> info.str + (end - start) + 1) = '\0';
755+ *(newstr->info.str.str + (end - start) + 1) = '\0';
756+ newstr->info.str.len = strlen(newstr->info.str.str);
715 return newstr;
757 return newstr;
716 }
758 }
717}
759}
718
760
719VAL idris_strRev(VM* vm, VAL str) {
761VAL idris_strRev(VM* vm, VAL str) {
720 char *xstr = GETSTR(str);
762 char *xstr = GETSTR(str);
763+ int xlen = GETSTRLEN(str);
764+
721− Closure* cl = allocate(sizeof(Closure) +
765+ Closure* cl = allocate(sizeof(Closure) + xlen + 1, 0);
722− strlen(xstr) + 1, 0);
723 SETTY(cl, CT_STRING);
766 SETTY(cl, CT_STRING);
724− cl->info.str = (char*)cl + sizeof(Closure);
767+ cl->info.str.str = (char*)cl + sizeof(Closure);
768+ cl->info.str.len = xlen;
725− idris_utf8_rev(xstr, cl->info.str);
769+ idris_utf8_rev(xstr, cl->info.str.str);
726 return cl;
770 return cl;
727}
771}
728
772
@@ -832,7 +876,7 @@ VAL doCopyTo(VM* vm, VAL x) {
832 cl = MKFLOATc(vm, x->info.f);
876 cl = MKFLOATc(vm, x->info.f);
833 break;
877 break;
834 case CT_STRING:
878 case CT_STRING:
835− cl = MKSTRc(vm, x->info.str);
879+ cl = MKSTRc(vm, x->info.str.str);
836 break;
880 break;
837 case CT_BIGINT:
881 case CT_BIGINT:
838 cl = MKBIGMc(vm, x->info.ptr);
882 cl = MKBIGMc(vm, x->info.ptr);
rts/idris_rts.h+20−3
@@ -42,6 +42,11 @@ typedef struct {
42 size_t offset;
42 size_t offset;
43} StrOffset;
43} StrOffset;
44
44
45+typedef struct {
46+ char* str;
47+ size_t len; // Cached strlen (we do 'strlen' a lot)
48+} String;
49+
45// A foreign pointer, managed by the idris GC
50// A foreign pointer, managed by the idris GC
46typedef struct {
51typedef struct {
47 size_t size;
52 size_t size;
@@ -59,7 +64,7 @@ typedef struct Closure {
59 con c;
64 con c;
60 int i;
65 int i;
61 double f;
66 double f;
62− char* str;
67+ String str;
63 StrOffset* str_offset;
68 StrOffset* str_offset;
64 void* ptr;
69 void* ptr;
65 uint8_t bits8;
70 uint8_t bits8;
@@ -182,7 +187,8 @@ typedef void(*func)(VM*, VAL*);
182#define ALIGN(__p, __alignment) ((__p + __alignment - 1) & ~(__alignment - 1))
187#define ALIGN(__p, __alignment) ((__p + __alignment - 1) & ~(__alignment - 1))
183
188
184// Retrieving values
189// 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))
186#define GETPTR(x) (((VAL)(x))->info.ptr)
192#define GETPTR(x) (((VAL)(x))->info.ptr)
187#define GETMPTR(x) (((VAL)(x))->info.mptr->data)
193#define GETMPTR(x) (((VAL)(x))->info.mptr->data)
188#define GETFLOAT(x) (((VAL)(x))->info.f)
194#define GETFLOAT(x) (((VAL)(x))->info.f)
@@ -229,7 +235,15 @@ typedef intptr_t i_int;
229
235
230// Stack management
236// Stack management
231
237
238+#ifdef IDRIS_TRACE
239+#define TRACE idris_trace(vm, __FUNCTION__, __LINE__);
240+#else
241+#define TRACE
242+#endif
243+
232−#define INITFRAME VAL* myoldbase
244+#define INITFRAME TRACE\
245+ VAL* myoldbase
246+
233#define REBASE vm->valstack_base = oldbase
247#define REBASE vm->valstack_base = oldbase
234#define RESERVE(x) if (vm->valstack_top+(x) > vm->stack_max) { stackOverflow(); } \
248#define RESERVE(x) if (vm->valstack_top+(x) > vm->stack_max) { stackOverflow(); } \
235 else { memset(vm->valstack_top, 0, (x)*sizeof(VAL)); }
249 else { memset(vm->valstack_top, 0, (x)*sizeof(VAL)); }
@@ -255,11 +269,13 @@ VAL MKCDATA(VM* vm, CHeapItem * item);
255VAL MKFLOATc(VM* vm, double val);
269VAL MKFLOATc(VM* vm, double val);
256VAL MKSTROFFc(VM* vm, StrOffset* off);
270VAL MKSTROFFc(VM* vm, StrOffset* off);
257VAL MKSTRc(VM* vm, char* str);
271VAL MKSTRc(VM* vm, char* str);
272+VAL MKSTRclen(VM* vm, char* str, int len);
258VAL MKPTRc(VM* vm, void* ptr);
273VAL MKPTRc(VM* vm, void* ptr);
259VAL MKMPTRc(VM* vm, void* ptr, size_t size);
274VAL MKMPTRc(VM* vm, void* ptr, size_t size);
260VAL MKCDATAc(VM* vm, CHeapItem * item);
275VAL MKCDATAc(VM* vm, CHeapItem * item);
261
276
262char* GETSTROFF(VAL stroff);
277char* GETSTROFF(VAL stroff);
278+size_t GETSTROFFLEN(VAL stroff);
263
279
264// #define SETTAG(x, a) (x)->info.c.tag = (a)
280// #define SETTAG(x, a) (x)->info.c.tag = (a)
265#define SETARG(x, i, a) ((x)->info.c.args)[i] = ((VAL)(a))
281#define SETARG(x, i, a) ((x)->info.c.args)[i] = ((VAL)(a))
@@ -340,6 +356,7 @@ VM* idris_getSender(Msg* msg);
340int idris_getChannel(Msg* msg);
356int idris_getChannel(Msg* msg);
341void idris_freeMsg(Msg* msg);
357void idris_freeMsg(Msg* msg);
342
358
359+void idris_trace(VM* vm, const char* func, int line);
343void dumpVal(VAL r);
360void dumpVal(VAL r);
344void dumpStack(VM* vm);
361void dumpStack(VM* vm);
345
362
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 :
5License : BSD3
5License : BSD3
6Maintainer : The Idris Community.
6Maintainer : The Idris Community.
7-}
7-}
8+{-# LANGUAGE FlexibleContexts #-}
9+
8module IRTS.CodegenC (codegenC) where
10module IRTS.CodegenC (codegenC) where
9
11
10−import Idris.AbsSyntax
12+import Idris.AbsSyntax hiding (getBC)
11import Idris.Core.TT
13import Idris.Core.TT
12import IRTS.Bytecode
14import IRTS.Bytecode
13import IRTS.CodegenCommon
15import IRTS.CodegenCommon
@@ -19,10 +21,12 @@ import IRTS.System
19import Util.System
21import Util.System
20
22
21import Control.Monad
23import Control.Monad
24+import Control.Monad
25+import Control.Monad.RWS
22import Data.Bits
26import Data.Bits
23import Data.Char
27import Data.Char
24−import Data.List (intercalate, nubBy)
28+import Data.List (find, intercalate, nubBy, partition)
25−import Debug.Trace
29+import qualified Data.Text as T
26import Numeric
30import Numeric
27import System.Directory
31import System.Directory
28import System.Exit
32import System.Exit
@@ -30,6 +34,8 @@ import System.FilePath ((<.>), (</>))
30import System.IO
34import System.IO
31import System.Process
35import System.Process
32
36
37+import Debug.Trace
38+
33codegenC :: CodeGenerator
39codegenC :: CodeGenerator
34codegenC ci = do codegenC' (simpleDecls ci)
40codegenC ci = do codegenC' (simpleDecls ci)
35 (outputFile ci)
41 (outputFile ci)
@@ -64,7 +70,9 @@ codegenC' defs out exec incs objs libs flags exports iface dbg
64 let bc = map toBC defs
70 let bc = map toBC defs
65 let wrappers = genWrappers bc
71 let wrappers = genWrappers bc
66 let h = concatMap toDecl (map fst bc)
72 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 })
68 let hi = concatMap ifaceC (concatMap getExp exports)
76 let hi = concatMap ifaceC (concatMap getExp exports)
69 d <- getIdrisCRTSDir
77 d <- getIdrisCRTSDir
70 mprog <- readFile (d </> "idris_main" <.> "c")
78 mprog <- readFile (d </> "idris_main" <.> "c")
@@ -134,12 +142,17 @@ creg Tmp = "REG1"
134toDecl :: Name -> String
142toDecl :: Name -> String
135toDecl f = "void " ++ cname f ++ "(VM*, VAL*);\n"
143toDecl f = "void " ++ cname f ++ "(VM*, VAL*);\n"
136
144
137−toC :: Name -> [BC] -> String
145+generateSrc :: [(Name, [BC])] -> RWS Int String CState ()
146+generateSrc bc = mapM_ toC bc
147+
148+toC :: (Name, [BC]) -> RWS Int String CState ()
138−toC f code
149+toC (f, code) = do
139− = -- "/* " ++ show code ++ "*/\n\n" ++
150+ modify (\s -> s { fnName = Just f })
151+ s <- get
140− "void " ++ cname f ++ "(VM* vm, VAL* oldbase) {\n" ++
152+ tell $ "void " ++ cname f ++ "(VM* vm, VAL* oldbase) {\n"
141− indent 1 ++ "INITFRAME;\n" ++
153+ tell $ indent (level s) ++ "INITFRAME;\n"
142− concatMap (bcc 1) code ++ "}\n\n"
154+ bcc code
155+ tell $ "}\n\n"
143
156
144showCStr :: String -> String
157showCStr :: String -> String
145showCStr s = '"' : foldr ((++) . showChar) "\"" s
158showCStr s = '"' : foldr ((++) . showChar) "\"" s
@@ -151,34 +164,46 @@ showCStr s = '"' : foldr ((++) . showChar) "\"" s
151 -- Note: we need the double quotes around the codes because otherwise
164 -- Note: we need the double quotes around the codes because otherwise
152 -- "\n3" would get encoded as "\x0a3", which is incorrect.
165 -- "\n3" would get encoded as "\x0a3", which is incorrect.
153 -- Instead, we opt for "\x0a""3" and let the C compiler deal with it.
166 -- 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)
156 | ord c < 0x7f = [c] -- 0x7f = \DEL
168 | ord c < 0x7f = [c] -- 0x7f = \DEL
157 | otherwise = showHexes (utf8bytes (ord c))
169 | otherwise = showHexes (utf8bytes (ord c))
158
170
159− utf8bytes :: Int -> [Int]
171+ showUTF8 c = "\"\"\\x" ++ pad (showHex c "") ++ "\"\""
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−
175 showHexes = foldr ((++) . showUTF8) ""
172 showHexes = foldr ((++) . showUTF8) ""
176− showUTF8 c = "\"\"\\x" ++ showHex c "\"\""
177
173
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+
178−bcc :: Int -> BC -> String
197+bcc :: [BC] -> RWS Int String CState ()
198+bcc [] = return ()
199+bcc ((ASSIGN l r):xs) = do
200+ i <- get
179−bcc i (ASSIGN l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"
201+ tell $ indent (level i) ++ creg l ++ " = " ++ creg r ++ ";\n"
202+ bcc xs
180−bcc i (ASSIGNCONST l c)
203+bcc ((ASSIGNCONST l c):xs) = do
204+ i <- get
181− = indent i ++ creg l ++ " = " ++ mkConst c ++ ";\n"
205+ tell $ indent (level i) ++ creg l ++ " = " ++ mkConst c ++ ";\n"
206+ bcc xs
182 where
207 where
183 mkConst (I i) = "MKINT(" ++ show i ++ ")"
208 mkConst (I i) = "MKINT(" ++ show i ++ ")"
184 mkConst (BI i) | i < (2^30) = "MKINT(" ++ show i ++ ")"
209 mkConst (BI i) | i < (2^30) = "MKINT(" ++ show i ++ ")"
@@ -196,16 +221,21 @@ bcc i (ASSIGNCONST l c)
196 mkConst c | isTypeConst c = "MKINT(42424242)"
221 mkConst c | isTypeConst c = "MKINT(42424242)"
197 mkConst c = error $ "mkConst of (" ++ show c ++ ") not implemented"
222 mkConst c = error $ "mkConst of (" ++ show c ++ ") not implemented"
198
223
224+bcc ((UPDATE l r):xs) = do
225+ i <- get
199−bcc i (UPDATE l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"
226+ tell $ indent (level i) ++ creg l ++ " = " ++ creg r ++ ";\n"
227+ bcc xs
200−bcc i (MKCON l loc tag []) | tag < 256
228+bcc ((MKCON l loc tag []):xs) | tag < 256 = do
229+ i <- get
201− = indent i ++ creg l ++ " = NULL_CON(" ++ show tag ++ ");\n"
230+ tell $ indent (level i) ++ creg l ++ " = NULL_CON(" ++ show tag ++ ");\n"
231+ bcc xs
202−bcc i (MKCON l loc tag args)
232+bcc ((MKCON l loc tag args):xs) = do
233+ i <- get
234+ let tab = indent (level i)
203− = indent i ++ alloc loc tag ++
235+ tell $ tab ++ alloc loc tag ++
204− indent i ++ setArgs 0 args ++ "\n" ++
236+ tab ++ setArgs 0 args ++ "\n" ++
205− indent i ++ creg l ++ " = " ++ creg Tmp ++ ";\n"
237+ tab ++ creg l ++ " = " ++ creg Tmp ++ ";\n"
206−
238+ bcc xs
207−-- "MKCON(vm, " ++ creg l ++ ", " ++ show tag ++ ", " ++
208−-- show (length args) ++ concatMap showArg args ++ ");\n"
209 where showArg r = ", " ++ creg r
239 where showArg r = ", " ++ creg r
210 setArgs i [] = ""
240 setArgs i [] = ""
211 setArgs i (x : xs) = "SETARG(" ++ creg Tmp ++ ", " ++ show i ++ ", " ++ creg x ++
241 setArgs i (x : xs) = "SETARG(" ++ creg Tmp ++ ", " ++ show i ++ ", " ++ creg x ++
@@ -217,52 +247,94 @@ bcc i (MKCON l loc tag args)
217 = "updateCon(" ++ creg Tmp ++ ", " ++ creg old ++ ", " ++ show tag ++ ", " ++
247 = "updateCon(" ++ creg Tmp ++ ", " ++ creg old ++ ", " ++ show tag ++ ", " ++
218 show (length args) ++ ");\n"
248 show (length args) ++ ");\n"
219
249
250+bcc ((PROJECT l loc a):xs) = do
251+ i <- get
220−bcc i (PROJECT l loc a) = indent i ++ "PROJECT(vm, " ++ creg l ++ ", " ++ show loc ++
252+ tell $ indent (level i) ++ "PROJECT(vm, " ++ creg l ++ ", "
221− ", " ++ show a ++ ");\n"
253+ ++ show loc ++ ", " ++ show a ++ ");\n"
254+ bcc xs
222−bcc i (PROJECTINTO r t idx)
255+bcc ((PROJECTINTO r t idx):xs) = do
256+ i <- get
223− = indent i ++ creg r ++ " = GETARG(" ++ creg t ++ ", " ++ show idx ++ ");\n"
257+ tell $ indent (level i) ++ creg r ++ " = GETARG(" ++ creg t
258+ ++ ", " ++ show idx ++ ");\n"
259+ bcc xs
224−bcc i (CASE True r code def)
260+bcc ((CASE True r code def):xs)
225− | length code < 4 = showCase i def code
261+ | length code < 4 = do
262+ showCases def code
263+ bcc xs
226 where
264 where
227− showCode :: Int -> [BC] -> String
265+ showCode bc = do
228− showCode i bc = "{\n" ++ concatMap (bcc (i + 1)) bc ++
266+ w <- getBC bc xs
267+ i <- get
229− indent i ++ "}\n"
268+ tell $ "{\n" ++ w ++ indent (level i) ++ "}\n"
230−
269+
231− showCase :: Int -> Maybe [BC] -> [(Int, [BC])] -> String
270+ showCases Nothing [(t, c)] = do
232− showCase i Nothing [(t, c)] = indent i ++ showCode i c
271+ i <- get
233− showCase i (Just def) [] = indent i ++ showCode i def
272+ tell $ indent (level i)
273+ showCode c
274+ showCases (Just def) [] = do
275+ i <- get
276+ tell $ indent (level i)
277+ showCode def
234− showCase i def ((t, c) : cs)
278+ showCases def ((t, c) : cs) = do
279+ i <- get
235− = indent i ++ "if (CTAG(" ++ creg r ++ ") == " ++ show t ++ ") " ++ showCode i c
280+ tell $ indent (level i) ++ "if (CTAG(" ++ creg r ++ ") == "
281+ ++ show t ++ ") "
282+ showCode c
236− ++ indent i ++ "else\n" ++ showCase i def cs
283+ tell $ indent (level i) ++ "else\n"
237−
284+ showCases def cs
285+
238−bcc i (CASE safe r code def)
286+bcc ((CASE safe r code def):xs) = do
287+ i <- get
239− = indent i ++ "switch(" ++ ctag safe ++ "(" ++ creg r ++ ")) {\n" ++
288+ tell $ indent (level i) ++ "switch(" ++ ctag safe ++ "(" ++ creg r ++ ")) {\n"
240− concatMap (showCase i) code ++
289+ mapM showCase code
241− showDef i def ++
290+ showDef def
242− indent i ++ "}\n"
291+ tell $ indent (level i) ++ "}\n"
292+ bcc xs
243 where
293 where
244 ctag True = "CTAG"
294 ctag True = "CTAG"
245 ctag False = "TAG"
295 ctag False = "TAG"
246
296
297+ showCase (t, bc) = do
298+ w <- getBC bc xs
299+ is <- get
300+ let i = level is
247− showCase i (t, bc) = indent i ++ "case " ++ show t ++ ":\n"
301+ tell $ indent i ++ "case " ++ show t ++ ":\n"
248− ++ concatMap (bcc (i+1)) bc ++ indent (i + 1) ++ "break;\n"
302+ ++ w ++ indent (i + 1) ++ "break;\n"
249− showDef i Nothing = ""
303+ showDef Nothing = return $ ()
250− showDef i (Just c) = indent i ++ "default:\n"
304+ showDef (Just c) = do
305+ w <- getBC c xs
306+ is <- get
307+ let i = level is
251− ++ concatMap (bcc (i+1)) c ++ indent (i + 1) ++ "break;\n"
308+ tell $ indent i ++ "default:\n" ++ w ++ indent (i + 1) ++ "break;\n"
309+
252−bcc i (CONSTCASE r code def)
310+bcc ((CONSTCASE r code def):xs)
253 | intConsts code
311 | intConsts code
254−-- = indent i ++ "switch(GETINT(" ++ creg r ++ ")) {\n" ++
312+ = do
255−-- concatMap (showCase i) code ++
313+ is <- get
256−-- showDef i def ++
314+ let i = level is
257−-- indent i ++ "}\n"
315+ codes <- mapM getCode code
258− = concatMap (iCase (creg r)) code ++
316+ defs <- showDefS def
259− indent i ++ "{\n" ++ showDefS i def ++ indent i ++ "}\n"
317+ tell $ concatMap (iCase i (creg r)) codes
318+ tell $ indent i ++ "{\n" ++ defs ++ indent i ++ "}\n"
319+ bcc xs
260 | strConsts code
320 | strConsts code
321+ = do
322+ is <- get
323+ let i = level is
324+ codes <- mapM getCode code
325+ defs <- showDefS def
261− = concatMap (strCase ("GETSTR(" ++ creg r ++ ")")) code ++
326+ tell $ concatMap (strCase i ("GETSTR(" ++ creg r ++ ")")) codes
262− indent i ++ "{\n" ++ showDefS i def ++ indent i ++ "}\n"
327+ ++ indent i ++ "{\n" ++ defs ++ indent i ++ "}\n"
328+ bcc xs
263 | bigintConsts code
329 | bigintConsts code
330+ = do
331+ is <- get
332+ let i = level is
333+ codes <- mapM getCode code
334+ defs <- showDefS def
264− = concatMap (biCase (creg r)) code ++
335+ tell $ concatMap (biCase i (creg r)) codes ++
265− indent i ++ "{\n" ++ showDefS i def ++ indent i ++ "}\n"
336+ indent i ++ "{\n" ++ defs ++ indent i ++ "}\n"
337+ bcc xs
266 | otherwise = error $ "Can't happen: Can't compile const case " ++ show code
338 | otherwise = error $ "Can't happen: Can't compile const case " ++ show code
267 where
339 where
268 intConsts ((I _, _ ) : _) = True
340 intConsts ((I _, _ ) : _) = True
@@ -279,72 +351,119 @@ bcc i (CONSTCASE r code def)
279 strConsts ((Str _, _ ) : _) = True
351 strConsts ((Str _, _ ) : _) = True
280 strConsts _ = False
352 strConsts _ = False
281
353
354+ getCode (x, code) = do
355+ c <- getBC code xs
356+ return (x, c)
357+
282− strCase sv (s, bc) =
358+ strCase i sv (s, bc) =
283 indent i ++ "if (strcmp(" ++ sv ++ ", " ++ show s ++ ") == 0) {\n" ++
359 indent i ++ "if (strcmp(" ++ sv ++ ", " ++ show s ++ ") == 0) {\n" ++
284− concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
360+ bc ++ indent i ++ "} else\n"
285− biCase bv (BI b, bc) =
361+ biCase i bv (BI b, bc) =
286 indent i ++ "if (bigEqConst(" ++ bv ++ ", " ++ show b ++ ")) {\n"
362 indent i ++ "if (bigEqConst(" ++ bv ++ ", " ++ show b ++ ")) {\n"
287− ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
363+ ++ bc ++ indent i ++ "} else\n"
288− iCase v (I b, bc) =
364+ iCase i v (I b, bc) =
289 indent i ++ "if (GETINT(" ++ v ++ ") == " ++ show b ++ ") {\n"
365 indent i ++ "if (GETINT(" ++ v ++ ") == " ++ show b ++ ") {\n"
290− ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
366+ ++ bc ++ indent i ++ "} else\n"
291− iCase v (Ch b, bc) =
367+ iCase i v (Ch b, bc) =
292 indent i ++ "if (GETINT(" ++ v ++ ") == " ++ show (fromEnum b) ++ ") {\n"
368 indent i ++ "if (GETINT(" ++ v ++ ") == " ++ show (fromEnum b) ++ ") {\n"
293− ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
369+ ++ bc ++ indent i ++ "} else\n"
294− iCase v (B8 w, bc) =
370+ iCase i v (B8 w, bc) =
295 indent i ++ "if (GETBITS8(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"
371 indent i ++ "if (GETBITS8(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"
296− ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
372+ ++ bc ++ indent i ++ "} else\n"
297− iCase v (B16 w, bc) =
373+ iCase i v (B16 w, bc) =
298 indent i ++ "if (GETBITS16(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"
374 indent i ++ "if (GETBITS16(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"
299− ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
375+ ++ bc ++ indent i ++ "} else\n"
300− iCase v (B32 w, bc) =
376+ iCase i v (B32 w, bc) =
301 indent i ++ "if (GETBITS32(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"
377 indent i ++ "if (GETBITS32(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"
302− ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
378+ ++ bc ++ indent i ++ "} else\n"
303− iCase v (B64 w, bc) =
379+ iCase i v (B64 w, bc) =
304 indent i ++ "if (GETBITS64(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"
380 indent i ++ "if (GETBITS64(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"
305− ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
381+ ++ bc ++ indent i ++ "} else\n"
306− showCase i (t, bc) = indent i ++ "case " ++ show t ++ ":\n"
382+
307− ++ concatMap (bcc (i+1)) bc ++
383+ showDefS Nothing = return ""
308− indent (i + 1) ++ "break;\n"
384+ showDefS (Just c) = getBC c xs
309− showDef i Nothing = ""
385+
310− showDef i (Just c) = indent i ++ "default:\n"
386+bcc (CALL n:xs) = do
311− ++ concatMap (bcc (i+1)) c ++
387+ i <- get
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"
388+ tell $ indent (level i) ++ "CALL(" ++ cname n ++ ");\n"
389+ bcc xs
390+bcc (TAILCALL n:xs) = do
391+ i <- get
317−bcc i (TAILCALL n) = indent i ++ "TAILCALL(" ++ cname n ++ ");\n"
392+ tell $ indent (level i) ++ "TAILCALL(" ++ cname n ++ ");\n"
393+ bcc xs
394+bcc ((SLIDE n):xs) = do
395+ i <- get
318−bcc i (SLIDE n) = indent i ++ "SLIDE(vm, " ++ show n ++ ");\n"
396+ tell $ indent (level i) ++ "SLIDE(vm, " ++ show n ++ ");\n"
397+ bcc xs
398+bcc (REBASE:xs) = do
399+ i <- get
319−bcc i REBASE = indent i ++ "REBASE;\n"
400+ tell $ indent (level i)++ "REBASE;\n"
401+ bcc xs
320−bcc i (RESERVE 0) = ""
402+bcc ((RESERVE 0):xs) = bcc xs
403+bcc ((RESERVE n):xs) = do
404+ i <- get
321−bcc i (RESERVE n) = indent i ++ "RESERVE(" ++ show n ++ ");\n"
405+ tell $ indent (level i) ++ "RESERVE(" ++ show n ++ ");\n"
406+ bcc xs
322−bcc i (ADDTOP 0) = ""
407+bcc ((ADDTOP 0):xs) = bcc xs
408+bcc ((ADDTOP n):xs) = do
409+ i <- get
323−bcc i (ADDTOP n) = indent i ++ "ADDTOP(" ++ show n ++ ");\n"
410+ tell $ indent (level i) ++ "ADDTOP(" ++ show n ++ ");\n"
411+ bcc xs
412+bcc ((TOPBASE n):xs) = do
413+ i <- get
324−bcc i (TOPBASE n) = indent i ++ "TOPBASE(" ++ show n ++ ");\n"
414+ tell $ indent (level i) ++ "TOPBASE(" ++ show n ++ ");\n"
415+ bcc xs
416+bcc ((BASETOP n):xs) = do
417+ i <- get
325−bcc i (BASETOP n) = indent i ++ "BASETOP(" ++ show n ++ ");\n"
418+ tell $ indent (level i) ++ "BASETOP(" ++ show n ++ ");\n"
419+ bcc xs
420+bcc (STOREOLD:xs) = do
421+ i <- get
326−bcc i STOREOLD = indent i ++ "STOREOLD;\n"
422+ tell $ indent (level i) ++ "STOREOLD;\n"
423+ bcc xs
424+bcc ((OP l fn args):xs) = do
425+ i <- get
327−bcc i (OP l fn args) = indent i ++ doOp (creg l ++ " = ") fn args ++ ";\n"
426+ tell $ indent (level i) ++ doOp (creg l ++ " = ") fn args ++ ";\n"
427+ bcc xs
328−bcc i (FOREIGNCALL l rty (FStr fn@('&':name)) [])
428+bcc ((FOREIGNCALL l rty (FStr fn@('&':name)) []):xs) = do
329− = indent i ++
429+ i <- get
330− c_irts (toFType rty) (creg l ++ " = ") fn ++ ";\n"
430+ tell $ indent (level i) ++ c_irts (toFType rty) (creg l ++ " = ") fn ++ ";\n"
431+ bcc xs
331−bcc i (FOREIGNCALL l rty (FStr fn) (x:xs)) | fn == "%wrapper"
432+bcc ((FOREIGNCALL l rty (FStr fn) (x:xs)):zs) | fn == "%wrapper"
332− = indent i ++
433+ = do
434+ i <- get
333− c_irts (toFType rty) (creg l ++ " = ")
435+ tell $ indent (level i) ++ c_irts (toFType rty) (creg l ++ " = ")
334 ("_idris_get_wrapper(" ++ creg (snd x) ++ ")") ++ ";\n"
436 ("_idris_get_wrapper(" ++ creg (snd x) ++ ")") ++ ";\n"
437+ bcc zs
335−bcc i (FOREIGNCALL l rty (FStr fn) (x:xs)) | fn == "%dynamic"
438+bcc ((FOREIGNCALL l rty (FStr fn) (x:xs)):zs) | fn == "%dynamic"
439+ = do
440+ i <- get
336− = indent i ++ c_irts (toFType rty) (creg l ++ " = ")
441+ tell $ indent (level i) ++ c_irts (toFType rty) (creg l ++ " = ")
337 ("(*(" ++ cFnSig "" rty xs ++ ") GETPTR(" ++ creg (snd x) ++ "))" ++
442 ("(*(" ++ cFnSig "" rty xs ++ ") GETPTR(" ++ creg (snd x) ++ "))" ++
338 "(" ++ showSep "," (map fcall xs) ++ ")") ++ ";\n"
443 "(" ++ showSep "," (map fcall xs) ++ ")") ++ ";\n"
444+ bcc zs
339−bcc i (FOREIGNCALL l rty (FStr fn) args)
445+bcc ((FOREIGNCALL l rty (FStr fn) args):xs) = do
340− = indent i ++
446+ i <- get
341− c_irts (toFType rty) (creg l ++ " = ")
447+ tell $ indent (level i) ++ c_irts (toFType rty) (creg l ++ " = ")
342− (fn ++ "(" ++ showSep "," (map fcall args) ++ ")") ++ ";\n"
448+ (fn ++ "(" ++ showSep "," (map fcall args) ++ ")") ++ ";\n"
449+ bcc xs
343−bcc i (FOREIGNCALL l rty _ args) = error "Foreign Function calls cannot be partially applied, without being inlined."
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
344−bcc i (NULL r) = indent i ++ creg r ++ " = NULL;\n" -- clear, so it'll be GCed
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, "
345−bcc i (ERROR str) = indent i ++ "fprintf(stderr, " ++ show str ++ "); fprintf(stderr, \"\\n\"); exit(-1);\n"
458+ ++ show str ++ "); fprintf(stderr, \"\\n\"); exit(-1);\n"
459+ bcc xs
346-- bcc i c = error (show c) -- indent i ++ "// not done yet\n"
460-- bcc i c = error (show c) -- indent i ++ "// not done yet\n"
347
461
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+
348fcall (t, arg) = irts_c (toFType t) (creg arg)
467fcall (t, arg) = irts_c (toFType t) (creg arg)
349-- Deconstruct the Foreign type in the defunctionalised expression and build
468-- Deconstruct the Foreign type in the defunctionalised expression and build
350-- a foreign type description for c_irts and irts_c
469-- a foreign type description for c_irts and irts_c
src/IRTS/Compiler.hs+2−1
@@ -5,7 +5,7 @@ Copyright :
5License : BSD3
5License : BSD3
6Maintainer : The Idris Community.
6Maintainer : The Idris Community.
7-}
7-}
8−{-# LANGUAGE CPP, PatternGuards, TypeSynonymInstances #-}
8+{-# LANGUAGE CPP, FlexibleContexts, PatternGuards, TypeSynonymInstances #-}
9
9
10module IRTS.Compiler(compile, generate) where
10module IRTS.Compiler(compile, generate) where
11
11
@@ -17,6 +17,7 @@ import Idris.Core.Evaluate
17import Idris.Core.TT
17import Idris.Core.TT
18import Idris.Erasure
18import Idris.Erasure
19import Idris.Error
19import Idris.Error
20+import Idris.Options
20import Idris.Output
21import Idris.Output
21import IRTS.CodegenC
22import IRTS.CodegenC
22import IRTS.CodegenCommon
23import IRTS.CodegenCommon
src/IRTS/Defunctionalise.hs+1−1
@@ -19,7 +19,7 @@ To defunctionalise:
198. Add explicit EVAL to case, primitives, and foreign calls
198. Add explicit EVAL to case, primitives, and foreign calls
20
20
21-}
21-}
22−{-# LANGUAGE PatternGuards #-}
22+{-# LANGUAGE FlexibleContexts, PatternGuards #-}
23module IRTS.Defunctionalise(module IRTS.Defunctionalise
23module IRTS.Defunctionalise(module IRTS.Defunctionalise
24 , module IRTS.Lang
24 , module IRTS.Lang
25 ) where
25 ) where
src/IRTS/JavaScript/AST.hs+8−19
@@ -99,35 +99,24 @@ data JsExpr
99
99
100translateChar :: Char -> String
100translateChar :: Char -> String
101translateChar ch
101translateChar ch
102− | '\a' <- ch = "\\u0007"
103 | '\b' <- ch = "\\b"
102 | '\b' <- ch = "\\b"
104 | '\f' <- ch = "\\f"
103 | '\f' <- ch = "\\f"
105 | '\n' <- ch = "\\n"
104 | '\n' <- ch = "\\n"
106 | '\r' <- ch = "\\r"
105 | '\r' <- ch = "\\r"
107 | '\t' <- ch = "\\t"
106 | '\t' <- ch = "\\t"
108 | '\v' <- ch = "\\v"
107 | '\v' <- ch = "\\v"
109− | '\SO' <- ch = "\\u000E"
110− | '\DEL' <- ch = "\\u007F"
111 | '\\' <- ch = "\\\\"
108 | '\\' <- ch = "\\\\"
112 | '\"' <- ch = "\\\""
109 | '\"' <- ch = "\\\""
113 | '\'' <- ch = "\\\'"
110 | '\'' <- ch = "\\\'"
111+ | ord ch < 0x20 = "\\x" ++ pad 2 (showHex (ord ch) "")
112+ | ord ch < 0x7f = [ch] -- 0x7f '\DEL'
114− | ch `elem` asciiTab = "\\u" ++ fill (showHex (ord ch) "")
113+ | ord ch <= 0xff = "\\x" ++ pad 2 (showHex (ord ch) "")
115− | ord ch > 255 = "\\u" ++ fill (showHex (ord ch) "")
114+ | ord ch <= 0xffff = "\\u" ++ pad 4 (showHex (ord ch) "")
116− | otherwise = [ch]
115+ | ord ch <= 0x10ffff = "\\u{" ++ showHex (ord ch) "}"
116+ | otherwise = error $ "Invalid Unicode code point U+" ++ showHex (ord ch) ""
117 where
117 where
118− fill :: String -> String
118+ pad :: Int -> String -> String
119− fill s = case length s of
119+ pad n s = replicate (n - length s) '0' ++ s
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−
131
120
132indent :: Text -> Text
121indent :: Text -> Text
133indent x =
122indent x =
src/IRTS/JavaScript/Codegen.hs+11−2
@@ -64,7 +64,14 @@ data CGConf = CGConf { header :: Text
64
64
65
65
66getInclude :: FilePath -> IO Text
66getInclude :: 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
68
75
69getIncludes :: [FilePath] -> IO Text
76getIncludes :: [FilePath] -> IO Text
70getIncludes l = do
77getIncludes l = do
@@ -76,6 +83,7 @@ includeLibs =
76 let
83 let
77 repl '\\' = '_'
84 repl '\\' = '_'
78 repl '/' = '_'
85 repl '/' = '_'
86+ repl '.' = '_'
79 repl c = c
87 repl c = c
80 in
88 in
81 concatMap (\lib -> "var " ++ (repl <$> lib) ++ " = require(\"" ++ lib ++"\");\n")
89 concatMap (\lib -> "var " ++ (repl <$> lib) ++ " = require(\"" ++ lib ++"\");\n")
@@ -90,7 +98,8 @@ codegenJs :: CGConf -> CodeGenerator
90codegenJs conf ci =
98codegenJs conf ci =
91 do
99 do
92 debug <- isYes <$> lookupEnv "IDRISJS_DEBUG"
100 debug <- isYes <$> lookupEnv "IDRISJS_DEBUG"
93− let defs = Map.fromList $ liftDecls ci
101+ let defs' = Map.fromList $ liftDecls ci
102+ let defs = globlToCon defs'
94 let used = Map.elems $ removeDeadCode defs [sMN 0 "runMain"]
103 let used = Map.elems $ removeDeadCode defs [sMN 0 "runMain"]
95 if debug then
104 if debug then
96 do
105 do
src/IRTS/JavaScript/LangTransforms.hs+13
@@ -8,6 +8,7 @@ Maintainer : The Idris Community.
8{-# LANGUAGE DeriveDataTypeable, OverloadedStrings, StandaloneDeriving #-}
8{-# LANGUAGE DeriveDataTypeable, OverloadedStrings, StandaloneDeriving #-}
9
9
10module IRTS.JavaScript.LangTransforms( removeDeadCode
10module IRTS.JavaScript.LangTransforms( removeDeadCode
11+ , globlToCon
11 ) where
12 ) where
12
13
13
14
@@ -94,3 +95,15 @@ removeDeadCode dcls start =
94 remCons = removeUnusedBranches (getUsedConstructors used) used
95 remCons = removeUnusedBranches (getUsedConstructors used) used
95 in if Map.keys remCons == Map.keys dcls then remCons
96 in if Map.keys remCons == Map.keys dcls then remCons
96 else removeDeadCode remCons start
97 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
28data JsPrimTy = PTBool | PTAny deriving (Eq, Ord)
28data JsPrimTy = PTBool | PTAny deriving (Eq, Ord)
29
29
30type PrimF = [JsExpr] -> JsExpr
30type 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
32
32
33deriving instance Ord PrimFn
33deriving instance Ord PrimFn
34
34
@@ -177,15 +177,22 @@ primDB =
177 , item (LZExt (ITFixed IT16) ITNative) False PTAny $ head
177 , item (LZExt (ITFixed IT16) ITNative) False PTAny $ head
178 , item (LZExt (ITFixed IT32) ITNative) False PTAny $ head
178 , item (LZExt (ITFixed IT32) ITNative) False PTAny $ head
179 , item (LZExt ITNative ITBig) True PTAny $ JsForeign "new $JSRTS.jsbn.BigInteger(''+%0)"
179 , 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
180 , item (LTrunc ITBig ITNative) True PTAny $ JsForeign "%0.intValue()|0"
184 , 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]
181 , item (LTrunc (ITFixed IT16) (ITFixed IT8)) False PTAny $ JsForeign "%0 & 0xFF"
190 , item (LTrunc (ITFixed IT16) (ITFixed IT8)) False PTAny $ JsForeign "%0 & 0xFF"
182 , item (LTrunc (ITFixed IT32) (ITFixed IT8)) False PTAny $ JsForeign "%0 & 0xFF"
191 , item (LTrunc (ITFixed IT32) (ITFixed IT8)) False PTAny $ JsForeign "%0 & 0xFF"
183 , item (LTrunc (ITFixed IT64) (ITFixed IT8)) True PTAny $ JsForeign "%0.intValue() & 0xFF"
192 , item (LTrunc (ITFixed IT64) (ITFixed IT8)) True PTAny $ JsForeign "%0.intValue() & 0xFF"
184 , item (LTrunc (ITFixed IT32) (ITFixed IT16)) False PTAny $ JsForeign "%0 & 0xFFFF"
193 , item (LTrunc (ITFixed IT32) (ITFixed IT16)) False PTAny $ JsForeign "%0 & 0xFFFF"
185 , item (LTrunc (ITFixed IT64) (ITFixed IT16)) True PTAny $ JsForeign "%0.intValue() & 0xFFFF"
194 , item (LTrunc (ITFixed IT64) (ITFixed IT16)) True PTAny $ JsForeign "%0.intValue() & 0xFFFF"
186 , item (LTrunc (ITFixed IT64) (ITFixed IT32)) True PTAny $ JsForeign "%0.intValue() & 0xFFFFFFFF"
195 , 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]
189 , item LStrConcat False PTAny $ binop "+"
196 , item LStrConcat False PTAny $ binop "+"
190 , item LStrLt False PTBool $ binop "<"
197 , item LStrLt False PTBool $ binop "<"
191 , item LStrEq False PTBool $ binop "=="
198 , item LStrEq False PTBool $ binop "=="
@@ -193,6 +200,7 @@ primDB =
193 , item (LIntFloat ITNative) False PTAny $ head
200 , item (LIntFloat ITNative) False PTAny $ head
194 , item (LIntFloat ITBig) True PTAny $ JsForeign "%0.intValue()"
201 , item (LIntFloat ITBig) True PTAny $ JsForeign "%0.intValue()"
195 , item (LFloatInt ITNative) False PTAny $ JsForeign "%0|0"
202 , item (LFloatInt ITNative) False PTAny $ JsForeign "%0|0"
203+ , item (LFloatInt ITBig) True PTAny $ JsForeign "new $JSRTS.jsbn.BigInteger(Math.trunc(%0)+ '')"
196 , item (LIntStr ITNative) False PTAny $ JsForeign "''+%0"
204 , item (LIntStr ITNative) False PTAny $ JsForeign "''+%0"
197 , item (LIntStr ITBig) True PTAny $ JsForeign "%0.toString()"
205 , item (LIntStr ITBig) True PTAny $ JsForeign "%0.toString()"
198 , item (LStrInt ITNative) False PTAny $ JsForeign "parseInt(%0)|0"
206 , item (LStrInt ITNative) False PTAny $ JsForeign "parseInt(%0)|0"
src/IRTS/Lang.hs+2−1
@@ -5,7 +5,8 @@ Copyright :
5License : BSD3
5License : BSD3
6Maintainer : The Idris Community.
6Maintainer : The Idris Community.
7-}
7-}
8−{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveGeneric, PatternGuards #-}
8+{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveGeneric, FlexibleContexts,
9+ PatternGuards #-}
9
10
10module IRTS.Lang where
11module IRTS.Lang where
11
12
src/IRTS/Portable.hs+1−1
@@ -5,7 +5,7 @@ Copyright :
5License : BSD3
5License : BSD3
6Maintainer : The Idris Community.
6Maintainer : The Idris Community.
7-}
7-}
8−{-# LANGUAGE OverloadedStrings #-}
8+{-# LANGUAGE FlexibleInstances, OverloadedStrings, TypeSynonymInstances #-}
9module IRTS.Portable (writePortable) where
9module IRTS.Portable (writePortable) where
10
10
11import Idris.Core.CaseTree
11import Idris.Core.CaseTree
src/IRTS/Simplified.hs+1
@@ -5,6 +5,7 @@ Copyright :
5License : BSD3
5License : BSD3
6Maintainer : The Idris Community.
6Maintainer : The Idris Community.
7-}
7-}
8+{-# LANGUAGE FlexibleContexts #-}
8module IRTS.Simplified(simplifyDefs, SDecl(..), SExp(..), SAlt(..)) where
9module IRTS.Simplified(simplifyDefs, SDecl(..), SExp(..), SAlt(..)) where
9
10
10import Idris.Core.CaseTree
11import Idris.Core.CaseTree
src/Idris/ASTUtils.hs+1
@@ -48,6 +48,7 @@ module Idris.ASTUtils(
48import Idris.AbsSyntaxTree
48import Idris.AbsSyntaxTree
49import Idris.Core.Evaluate
49import Idris.Core.Evaluate
50import Idris.Core.TT
50import Idris.Core.TT
51+import Idris.Options
51
52
52import Prelude hiding (id, (.))
53import Prelude hiding (id, (.))
53
54
src/Idris/AbsSyntax.hs+3−124
@@ -6,7 +6,7 @@ License : BSD3
6Maintainer : The Idris Community.
6Maintainer : The Idris Community.
7-}
7-}
8
8
9−{-# LANGUAGE DeriveFunctor, PatternGuards #-}
9+{-# LANGUAGE DeriveFunctor, FlexibleContexts, PatternGuards #-}
10
10
11module Idris.AbsSyntax(
11module Idris.AbsSyntax(
12 module Idris.AbsSyntax
12 module Idris.AbsSyntax
@@ -19,6 +19,7 @@ import Idris.Core.Evaluate
19import Idris.Core.TT
19import Idris.Core.TT
20import Idris.Docstrings
20import Idris.Docstrings
21import Idris.IdeMode hiding (Opt(..))
21import Idris.IdeMode hiding (Opt(..))
22+import Idris.Options
22import IRTS.CodegenCommon
23import IRTS.CodegenCommon
23
24
24import System.Directory (canonicalizePath, doesFileExist)
25import System.Directory (canonicalizePath, doesFileExist)
@@ -2602,126 +2603,4 @@ mkUniqueNames env shadows tm
2602
2603
2603 mkUniq ql nmap tm = descendM (mkUniq ql nmap) tm
2604 mkUniq ql nmap tm = descendM (mkUniq ql nmap) tm
2604
2605
2605−getFile :: Opt -> Maybe String
2606+
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
src/Idris/AbsSyntaxTree.hs+13−134
@@ -6,7 +6,9 @@ License : BSD3
6Maintainer : The Idris Community.
6Maintainer : The Idris Community.
7-}
7-}
8
8
9−{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveGeneric, PatternGuards #-}
9+{-# LANGUAGE DeriveDataTypeable, DeriveFoldable, DeriveFunctor, DeriveGeneric,
10+ DeriveTraversable, FlexibleContexts, FlexibleInstances,
11+ MultiParamTypeClasses, PatternGuards, TypeSynonymInstances #-}
10
12
11module Idris.AbsSyntaxTree where
13module Idris.AbsSyntaxTree where
12
14
@@ -14,6 +16,7 @@ import Idris.Core.Elaborate hiding (Tactic(..))
14import Idris.Core.Evaluate
16import Idris.Core.Evaluate
15import Idris.Core.TT
17import Idris.Core.TT
16import Idris.Docstrings
18import Idris.Docstrings
19+import Idris.Options
17import IRTS.CodegenCommon
20import IRTS.CodegenCommon
18import IRTS.Lang
21import IRTS.Lang
19import Util.DynamicLinker
22import Util.DynamicLinker
@@ -146,8 +149,7 @@ data PPOption = PPOption {
146 , ppopt_depth :: Maybe Int
149 , ppopt_depth :: Maybe Int
147 } deriving (Show)
150 } deriving (Show)
148
151
149−data Optimisation = PETransform -- ^ partial eval and associated transforms
152+
150− deriving (Show, Eq, Generic)
151
153
152defaultOptimise :: [Optimisation]
154defaultOptimise :: [Optimisation]
153defaultOptimise = []
155defaultOptimise = []
@@ -183,21 +185,12 @@ ppOption opt = PPOption {
183ppOptionIst :: IState -> PPOption
185ppOptionIst :: IState -> PPOption
184ppOptionIst = ppOption . idris_options
186ppOptionIst = ppOption . idris_options
185
187
186−data LanguageExt = TypeProviders | ErrorReflection | UniquenessTypes
187− | DSLNotation | ElabReflection | FCReflection
188− | LinearTypes
189− deriving (Show, Eq, Read, Ord, Generic)
190
188
191-- | The output mode in use
189-- | The output mode in use
192data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle
190data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle
193 | IdeMode Integer Handle -- ^ Send IDE output for some request ID to the handle
191 | IdeMode Integer Handle -- ^ Send IDE output for some request ID to the handle
194 deriving Show
192 deriving Show
195
193
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)
201
194
202-- | If a function has no totality annotation, what do we assume?
195-- | If a function has no totality annotation, what do we assume?
203data DefaultTotality = DefaultCheckingTotal -- ^ Total
196data DefaultTotality = DefaultCheckingTotal -- ^ Total
@@ -434,53 +427,7 @@ throwError = Trans.lift . throwE
434
427
435-- Commands in the REPL
428-- Commands in the REPL
436
429
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
444
430
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− ]
484
431
485
432
486data ElabShellCmd = EQED
433data ElabShellCmd = EQED
@@ -494,83 +441,8 @@ data ElabShellCmd = EQED
494 | EDocStr (Either Name Const)
441 | EDocStr (Either Name Const)
495 deriving (Show, Eq)
442 deriving (Show, Eq)
496
443
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)
571
444
572−data REPLPort = DontListen | ListenPort PortNumber
445+
573− deriving (Eq, Generic, Show)
574
446
575-- Parsed declarations
447-- Parsed declarations
576
448
@@ -1177,6 +1049,7 @@ mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
1177 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
1049 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
1178 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1050 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1179 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1051 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)
1180mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
1053mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
1181mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
1054mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
1182mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
1055mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
@@ -1301,6 +1174,7 @@ data PDo' t = DoExp FC t
1301 | DoBindP FC t t [(t,t)]
1174 | DoBindP FC t t [(t,t)]
1302 | DoLet FC Name FC t t -- ^ second FC is precise name location
1175 | DoLet FC Name FC t t -- ^ second FC is precise name location
1303 | DoLetP FC t t
1176 | DoLetP FC t t
1177+ | DoRewrite FC t -- rewrite in do block
1304 deriving (Eq, Ord, Functor, Data, Generic, Typeable)
1178 deriving (Eq, Ord, Functor, Data, Generic, Typeable)
1305{-!
1179{-!
1306deriving instance Binary PDo'
1180deriving instance Binary PDo'
@@ -1312,6 +1186,7 @@ instance Sized a => Sized (PDo' a) where
1312 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1186 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1313 size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
1187 size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
1314 size (DoLetP fc l r) = 1 + size fc + size l + size r
1188 size (DoLetP fc l r) = 1 + size fc + size l + size r
1189+ size (DoRewrite fc h) = 1 + size fc + size h
1315
1190
1316type PDo = PDo' PTerm
1191type PDo = PDo' PTerm
1317
1192
@@ -1407,6 +1282,7 @@ highestFC (PDoBlock lines) =
1407 getDoFC (DoBindP fc l r alts) = fc
1282 getDoFC (DoBindP fc l r alts) = fc
1408 getDoFC (DoLet fc nm nfc l r) = fc
1283 getDoFC (DoLet fc nm nfc l r) = fc
1409 getDoFC (DoLetP fc l r) = fc
1284 getDoFC (DoLetP fc l r) = fc
1285+ getDoFC (DoRewrite fc h) = fc
1410
1286
1411highestFC (PIdiom fc _) = Just fc
1287highestFC (PIdiom fc _) = Just fc
1412highestFC (PMetavar fc _) = Just fc
1288highestFC (PMetavar fc _) = Just fc
@@ -2081,6 +1957,9 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
2081 ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab
1957 ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab
2082 text "no pretty printer for pattern-matching do binding" :
1958 text "no pretty printer for pattern-matching do binding" :
2083 ppdo bnd dos
1959 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
2084 ppdo _ [] = []
1963 ppdo _ [] = []
2085 prettySe d p bnd (PCoerced t) = prettySe d p bnd t
1964 prettySe d p bnd (PCoerced t) = prettySe d p bnd t
2086 prettySe d p bnd (PElabError s) = pretty s
1965 prettySe d p bnd (PElabError s) = pretty s
src/Idris/Apropos.hs+1
@@ -5,6 +5,7 @@ Copyright :
5License : BSD3
5License : BSD3
6Maintainer : The Idris Community.
6Maintainer : The Idris Community.
7-}
7-}
8+{-# LANGUAGE FlexibleInstances #-}
8module Idris.Apropos (apropos, aproposModules) where
9module Idris.Apropos (apropos, aproposModules) where
9
10
10import Idris.AbsSyntax
11import 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.
17names over '_', patterns over names, etc.
17names over '_', patterns over names, etc.
18-}
18-}
19
19
20−{-# LANGUAGE PatternGuards #-}
20+{-# LANGUAGE FlexibleContexts, PatternGuards #-}
21
21
22module Idris.CaseSplit(
22module Idris.CaseSplit(
23 splitOnLine, replaceSplits
23 splitOnLine, replaceSplits
src/Idris/Chaser.hs+2
@@ -5,6 +5,8 @@ Copyright :
5License : BSD3
5License : BSD3
6Maintainer : The Idris Community.
6Maintainer : The Idris Community.
7-}
7-}
8+{-# LANGUAGE FlexibleContexts #-}
9+
8module Idris.Chaser(
10module Idris.Chaser(
9 buildTree, getImports
11 buildTree, getImports
10 , getModuleFiles
12 , getModuleFiles
src/Idris/CmdOptions.hs+1−6
@@ -16,11 +16,8 @@ module Idris.CmdOptions
16 , getPkgREPL, getPkgTest, getPort, getIBCSubDir
16 , getPkgREPL, getPkgTest, getPort, getIBCSubDir
17 ) where
17 ) where
18
18
19−import Idris.AbsSyntax (getClient, getIBCSubDir, getPkg, getPkgCheck,
20− getPkgClean, getPkgMkDoc, getPkgREPL, getPkgTest,
21− getPort, opt)
22−import Idris.AbsSyntaxTree
23import Idris.Info (getIdrisVersion)
19import Idris.Info (getIdrisVersion)
20+import Idris.Options
24import IRTS.CodegenCommon
21import IRTS.CodegenCommon
25
22
26import Control.Monad.Trans (lift)
23import Control.Monad.Trans (lift)
@@ -28,9 +25,7 @@ import Control.Monad.Trans.Except (throwE)
28import Control.Monad.Trans.Reader (ask)
25import Control.Monad.Trans.Reader (ask)
29import Data.Char
26import Data.Char
30import Data.Maybe
27import Data.Maybe
31−#if MIN_VERSION_optparse_applicative(0,13,0)
32import Data.Monoid ((<>))
28import Data.Monoid ((<>))
33−#endif
34import Options.Applicative
29import Options.Applicative
35import Options.Applicative.Arrows
30import Options.Applicative.Arrows
36import Options.Applicative.Types (ReadM(..))
31import Options.Applicative.Types (ReadM(..))
src/Idris/Core/Binary.hs+2
@@ -5,6 +5,8 @@ Copyright :
5License : BSD3
5License : BSD3
6Maintainer : The Idris Community.
6Maintainer : The Idris Community.
7-}
7-}
8+{-# LANGUAGE FlexibleInstances #-}
9+
8{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
10{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
9module Idris.Core.Binary where
11module Idris.Core.Binary where
10
12
src/Idris/Core/CaseTree.hs+2−2
@@ -18,8 +18,8 @@ allows casing on arbitrary terms, here we choose to maintain the distinction
18in order to allow for better optimisation opportunities.
18in order to allow for better optimisation opportunities.
19
19
20-}
20-}
21+{-# LANGUAGE DeriveFunctor, DeriveGeneric, FlexibleContexts, FlexibleInstances,
21−{-# LANGUAGE DeriveFunctor, DeriveGeneric, PatternGuards, TypeSynonymInstances
22+ PatternGuards, TypeSynonymInstances #-}
22− #-}
23
23
24module Idris.Core.CaseTree (
24module Idris.Core.CaseTree (
25 CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..), ErasureInfo
25 CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..), ErasureInfo
src/Idris/Core/DeepSeq.hs+4−1
@@ -5,7 +5,8 @@ Copyright :
5License : BSD3
5License : BSD3
6Maintainer : The Idris Community.
6Maintainer : The Idris Community.
7-}
7-}
8+{-# LANGUAGE BangPatterns, CPP, FlexibleInstances, TypeSynonymInstances,
8−{-# LANGUAGE BangPatterns, ViewPatterns #-}
9+ ViewPatterns #-}
9{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
10{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
10
11
11module Idris.Core.DeepSeq where
12module Idris.Core.DeepSeq where
@@ -27,7 +28,9 @@ forceDefCtxt (force -> !ctxt) = ctxt
27
28
28instance NFData NameOutput
29instance NFData NameOutput
29instance NFData TextFormatting
30instance NFData TextFormatting
31+#if !(MIN_VERSION_base(4,10,0))
30instance NFData Ordering
32instance NFData Ordering
33+#endif
31instance NFData OutputAnnotation
34instance NFData OutputAnnotation
32instance NFData SpecialName
35instance NFData SpecialName
33instance NFData Universe
36instance NFData Universe
src/Idris/Core/ProofState.hs+2−1
@@ -10,7 +10,8 @@ proofs, and some high level commands for introducing new theorems,
10evaluation/checking inside the proof system, etc.
10evaluation/checking inside the proof system, etc.
11-}
11-}
12
12
13−{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, PatternGuards #-}
13+{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses,
14+ PatternGuards #-}
14module Idris.Core.ProofState(
15module Idris.Core.ProofState(
15 ProofState(..), newProof, envAtFocus, goalAtFocus
16 ProofState(..), newProof, envAtFocus, goalAtFocus
16 , Tactic(..), Goal(..), processTactic, nowElaboratingPS
17 , 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:
22 * We have a simple collection of tactics which we use to elaborate source
22 * We have a simple collection of tactics which we use to elaborate source
23 programs with implicit syntax into fully explicit terms.
23 programs with implicit syntax into fully explicit terms.
24-}
24-}
25−{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveGeneric, FlexibleContexts,
25+{-# LANGUAGE DeriveDataTypeable, DeriveFoldable, DeriveFunctor, DeriveGeneric,
26+ DeriveTraversable, FlexibleContexts, FlexibleInstances,
26− FunctionalDependencies, MultiParamTypeClasses, PatternGuards #-}
27+ FunctionalDependencies, MultiParamTypeClasses, PatternGuards,
28+ TypeSynonymInstances #-}
27{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
29{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
28module Idris.Core.TT(
30module Idris.Core.TT(
29 AppStatus(..), ArithTy(..), Binder(..), Const(..), Ctxt(..)
31 AppStatus(..), ArithTy(..), Binder(..), Const(..), Ctxt(..)
src/Idris/Core/Typecheck.hs+2−2
@@ -6,8 +6,8 @@ License : BSD3
6Maintainer : The Idris Community.
6Maintainer : The Idris Community.
7-}
7-}
8
8
9−{-# LANGUAGE DeriveFunctor, FlexibleInstances, MultiParamTypeClasses,
9+{-# LANGUAGE DeriveFunctor, FlexibleContexts, FlexibleInstances,
10− PatternGuards #-}
10+ MultiParamTypeClasses, PatternGuards #-}
11
11
12module Idris.Core.Typecheck where
12module Idris.Core.Typecheck where
13
13
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
11a list of things which need to be injective.
11a list of things which need to be injective.
12
12
13-}
13-}
14−{-# LANGUAGE PatternGuards #-}
14+{-# LANGUAGE FlexibleContexts, PatternGuards #-}
15
15
16module Idris.Core.Unify(
16module Idris.Core.Unify(
17 match_unify, unify
17 match_unify, unify
src/Idris/Core/WHNF.hs+1−1
@@ -6,7 +6,7 @@ License : BSD3
6Maintainer : The Idris Community.
6Maintainer : The Idris Community.
7-}
7-}
8
8
9−{-# LANGUAGE PatternGuards #-}
9+{-# LANGUAGE FlexibleContexts, PatternGuards #-}
10{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
10{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
11module Idris.Core.WHNF(whnf, whnfArgs, WEnv) where
11module Idris.Core.WHNF(whnf, whnfArgs, WEnv) where
12
12
src/Idris/Coverage.hs+1−1
@@ -5,7 +5,7 @@ Copyright :
5License : BSD3
5License : BSD3
6Maintainer : The Idris Community.
6Maintainer : The Idris Community.
7-}
7-}
8−{-# LANGUAGE PatternGuards #-}
8+{-# LANGUAGE FlexibleContexts, PatternGuards #-}
9module Idris.Coverage(genClauses, validCoverageCase, recoverableCoverage,
9module Idris.Coverage(genClauses, validCoverageCase, recoverableCoverage,
10 mkPatTm) where
10 mkPatTm) where
11
11
src/Idris/DSL.hs+2
@@ -109,6 +109,8 @@ expandSugar dsl (PDoBlock ds)
109 = PLet fc n nfc ty tm (block b rest)
109 = PLet fc n nfc ty tm (block b rest)
110 block b (DoLetP fc p tm : rest)
110 block b (DoLetP fc p tm : rest)
111 = PCase fc tm [(p, block b rest)]
111 = PCase fc tm [(p, block b rest)]
112+ block b (DoRewrite fc h : rest)
113+ = PRewrite fc Nothing h (block b rest) Nothing
112 block b (DoExp fc tm : rest)
114 block b (DoExp fc tm : rest)
113 = PApp fc b
115 = PApp fc b
114 [pexp tm,
116 [pexp tm,
src/Idris/DataOpts.hs+1−1
@@ -5,7 +5,7 @@ Copyright :
5License : BSD3
5License : BSD3
6Maintainer : The Idris Community.
6Maintainer : The Idris Community.
7-}
7-}
8−{-# LANGUAGE PatternGuards #-}
8+{-# LANGUAGE FlexibleInstances, PatternGuards #-}
9
9
10module Idris.DataOpts(applyOpts) where
10module Idris.DataOpts(applyOpts) where
11
11
src/Idris/DeepSeq.hs+1
@@ -18,6 +18,7 @@ import Idris.Core.DeepSeq
18import Idris.Core.TT
18import Idris.Core.TT
19import Idris.Docstrings
19import Idris.Docstrings
20import qualified Idris.Docstrings as D
20import qualified Idris.Docstrings as D
21+import Idris.Options
21import IRTS.CodegenCommon (OutputType(..))
22import IRTS.CodegenCommon (OutputType(..))
22import IRTS.Lang (PrimFn(..))
23import IRTS.Lang (PrimFn(..))
23
24
src/Idris/Docs.hs+2−1
@@ -15,7 +15,7 @@ module Idris.Docs (
15 , FunDoc, FunDoc'(..), Docs, Docs'(..)
15 , FunDoc, FunDoc'(..), Docs, Docs'(..)
16 ) where
16 ) where
17
17
18−import Idris.AbsSyntax (FixDecl(..), Fixity, HowMuchDocs(..), IState(..), Idris,
18+import Idris.AbsSyntax (FixDecl(..), Fixity, IState(..), Idris,
19 InterfaceInfo(..), PArg'(..), PDecl'(..), PPOption(..),
19 InterfaceInfo(..), PArg'(..), PDecl'(..), PPOption(..),
20 PTerm(..), Plicity(..), RecordInfo(..), basename,
20 PTerm(..), Plicity(..), RecordInfo(..), basename,
21 getIState, modDocName, ppOptionIst, pprintPTerm,
21 getIState, modDocName, ppOptionIst, pprintPTerm,
@@ -26,6 +26,7 @@ import Idris.Delaborate
26import Idris.Docstrings (DocTerm, Docstring, emptyDocstring, noDocs,
26import Idris.Docstrings (DocTerm, Docstring, emptyDocstring, noDocs,
27 nullDocstring, overview, renderDocTerm,
27 nullDocstring, overview, renderDocTerm,
28 renderDocstring)
28 renderDocstring)
29+import Idris.Options (HowMuchDocs(..))
29
30
30import Util.Pretty
31import Util.Pretty
31
32
src/Idris/Docstrings.hs+2−1
@@ -6,7 +6,8 @@ License : BSD3
6Maintainer : The Idris Community.
6Maintainer : The Idris Community.
7-}
7-}
8
8
9−{-# LANGUAGE DeriveFunctor, DeriveGeneric, ScopedTypeVariables #-}
9+{-# LANGUAGE DeriveFoldable, DeriveFunctor, DeriveGeneric, DeriveTraversable,
10+ ScopedTypeVariables #-}
10{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
11{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
11module Idris.Docstrings (
12module Idris.Docstrings (
12 Docstring(..), Block(..), Inline(..), parseDocstring, renderDocstring
13 Docstring(..), Block(..), Inline(..), parseDocstring, renderDocstring
src/Idris/Elab/Clause.hs+1
@@ -31,6 +31,7 @@ import Idris.Elab.Utils
31import Idris.Error
31import Idris.Error
32import Idris.Imports
32import Idris.Imports
33import Idris.Inliner
33import Idris.Inliner
34+import Idris.Options
34import Idris.Output (iRenderResult, iWarn, iputStrLn, pshow, sendHighlighting)
35import Idris.Output (iRenderResult, iWarn, iputStrLn, pshow, sendHighlighting)
35import Idris.PartialEval
36import Idris.PartialEval
36import Idris.Primitives
37import Idris.Primitives
src/Idris/Elab/Provider.hs+1
@@ -30,6 +30,7 @@ import Idris.Elab.Value
30import Idris.Error
30import Idris.Error
31import Idris.Imports
31import Idris.Imports
32import Idris.Inliner
32import Idris.Inliner
33+import Idris.Options
33import Idris.Output (iWarn, iputStrLn, pshow)
34import Idris.Output (iWarn, iputStrLn, pshow)
34import Idris.PartialEval
35import Idris.PartialEval
35import Idris.Primitives
36import Idris.Primitives
src/Idris/Elab/Quasiquote.hs+1
@@ -75,6 +75,7 @@ extractDoUnquotes d (DoLet fc n nfc v b)
75 (b', ex2) <- extractUnquotes d b
75 (b', ex2) <- extractUnquotes d b
76 return (DoLet fc n nfc v' b', ex1 ++ ex2)
76 return (DoLet fc n nfc v' b', ex1 ++ ex2)
77extractDoUnquotes d (DoLetP fc t t') = fail "Pattern-matching lets cannot be quasiquoted"
77extractDoUnquotes 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"
78
79
79
80
80extractUnquotes :: Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
81extractUnquotes :: Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
src/Idris/Elab/Term.hs+5−2
@@ -27,6 +27,7 @@ import Idris.Elab.Rewrite
27import Idris.Elab.Utils
27import Idris.Elab.Utils
28import Idris.Error
28import Idris.Error
29import Idris.ErrReverse (errReverse)
29import Idris.ErrReverse (errReverse)
30+import Idris.Options
30import Idris.Output (pshow)
31import Idris.Output (pshow)
31import Idris.ProofSearch
32import Idris.ProofSearch
32import Idris.Reflection
33import Idris.Reflection
@@ -2658,9 +2659,11 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
2658 concat (intersperse ", " (map show handlers))
2659 concat (intersperse ", " (map show handlers))
2659 let reports = map (\n -> RApp (Var n) (reflectErr err)) handlers
2660 let reports = map (\n -> RApp (Var n) (reflectErr err)) handlers
2660
2661
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.
2662 handlers <- case mapM (check (tt_ctxt ist) []) reports of
2665 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
2664 OK hs -> return hs
2667 OK hs -> return hs
2665
2668
2666 -- Normalize error handler terms to produce the new messages
2669 -- Normalize error handler terms to produce the new messages
src/Idris/Elab/Type.hs+1
@@ -32,6 +32,7 @@ import Idris.Elab.Value
32import Idris.Error
32import Idris.Error
33import Idris.Imports
33import Idris.Imports
34import Idris.Inliner
34import Idris.Inliner
35+import Idris.Options
35import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
36import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
36import Idris.PartialEval
37import Idris.PartialEval
37import Idris.Primitives
38import Idris.Primitives
src/Idris/Elab/Utils.hs+7−6
@@ -5,7 +5,7 @@ Copyright :
5License : BSD3
5License : BSD3
6Maintainer : The Idris Community.
6Maintainer : The Idris Community.
7-}
7-}
8−{-# LANGUAGE PatternGuards #-}
8+{-# LANGUAGE FlexibleContexts, PatternGuards #-}
9module Idris.Elab.Utils where
9module Idris.Elab.Utils where
10
10
11import Idris.AbsSyntax
11import Idris.AbsSyntax
@@ -449,9 +449,12 @@ displayWarnings est
449 = mapM_ displayImpWarning (implicit_warnings est)
449 = mapM_ displayImpWarning (implicit_warnings est)
450 where
450 where
451 displayImpWarning :: (FC, Name) -> Idris ()
451 displayImpWarning :: (FC, Name) -> Idris ()
452− displayImpWarning (fc, n) =
452+ displayImpWarning (fc, n) = do
453+ ist <- getIState
454+ let msg = show (nsroot n)
453− iputStrLn $ show fc ++ ":WARNING: " ++ show (nsroot n) ++ " is bound as an implicit\n"
455+ ++ " is bound as an implicit\n"
454− ++ "\tDid you mean to refer to " ++ show n ++ "?"
456+ ++ "\tDid you mean to refer to " ++ show n ++ "?"
457+ iWarn fc (pprintErr ist (Msg msg))
455
458
456propagateParams :: IState -> [Name] -> Type -> [Name] -> PTerm -> PTerm
459propagateParams :: IState -> [Name] -> Type -> [Name] -> PTerm -> PTerm
457propagateParams i ps t bound tm@(PApp _ (PRef fc hls n) args)
460propagateParams i ps t bound tm@(PApp _ (PRef fc hls n) args)
@@ -767,5 +770,3 @@ isPlausible ist var env n ty
767 collectConstraints env tcs t
770 collectConstraints env tcs t
768 | (V i, _) <- unApply t = (Just (env !! i), tcs)
771 | (V i, _) <- unApply t = (Just (env !! i), tcs)
769 | otherwise = (Nothing, tcs)
772 | otherwise = (Nothing, tcs)
770−
771−
src/Idris/ElabDecls.hs+1
@@ -41,6 +41,7 @@ import Idris.Elab.Value
41import Idris.Error
41import Idris.Error
42import Idris.Imports
42import Idris.Imports
43import Idris.Inliner
43import Idris.Inliner
44+import Idris.Options
44import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
45import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
45import Idris.PartialEval
46import Idris.PartialEval
46import Idris.Primitives
47import Idris.Primitives
src/Idris/Erasure.hs+1
@@ -15,6 +15,7 @@ import Idris.Core.CaseTree
15import Idris.Core.Evaluate
15import Idris.Core.Evaluate
16import Idris.Core.TT
16import Idris.Core.TT
17import Idris.Error
17import Idris.Error
18+import Idris.Options
18import Idris.Primitives
19import Idris.Primitives
19
20
20import Prelude hiding (id, (.))
21import Prelude hiding (id, (.))
src/Idris/Error.hs+1
@@ -138,6 +138,7 @@ warnDisamb ist (PDoBlock steps) = mapM_ wStep steps
138 mapM_ (\(x,y) -> warnDisamb ist x >> warnDisamb ist y) cs
138 mapM_ (\(x,y) -> warnDisamb ist x >> warnDisamb ist y) cs
139 wStep (DoLet _ _ _ x y) = warnDisamb ist x >> warnDisamb ist y
139 wStep (DoLet _ _ _ x y) = warnDisamb ist x >> warnDisamb ist y
140 wStep (DoLetP _ x y) = warnDisamb ist x >> warnDisamb ist y
140 wStep (DoLetP _ x y) = warnDisamb ist x >> warnDisamb ist y
141+ wStep (DoRewrite _ h) = warnDisamb ist h
141warnDisamb ist (PIdiom _ x) = warnDisamb ist x
142warnDisamb ist (PIdiom _ x) = warnDisamb ist x
142warnDisamb ist (PMetavar _ _) = return ()
143warnDisamb ist (PMetavar _ _) = return ()
143warnDisamb ist (PProof tacs) = mapM_ (Foldable.mapM_ (warnDisamb ist)) tacs
144warnDisamb ist (PProof tacs) = mapM_ (Foldable.mapM_ (warnDisamb ist)) tacs
src/Idris/IBC.hs+9−1
@@ -5,7 +5,7 @@ Copyright :
5License : BSD3
5License : BSD3
6Maintainer : The Idris Community.
6Maintainer : The Idris Community.
7-}
7-}
8−{-# LANGUAGE TypeSynonymInstances #-}
8+{-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}
9{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
9{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
10
10
11module Idris.IBC (loadIBC, loadPkgIndex,
11module Idris.IBC (loadIBC, loadPkgIndex,
@@ -23,6 +23,7 @@ import Idris.Docstrings (Docstring)
23import qualified Idris.Docstrings as D
23import qualified Idris.Docstrings as D
24import Idris.Error
24import Idris.Error
25import Idris.Imports
25import Idris.Imports
26+import Idris.Options
26import Idris.Output
27import Idris.Output
27import IRTS.System (getIdrisLibDir)
28import IRTS.System (getIdrisLibDir)
28
29
@@ -2292,6 +2293,9 @@ instance (Binary t) => Binary (PDo' t) where
2292 put x1
2293 put x1
2293 put x2
2294 put x2
2294 put x3
2295 put x3
2296+ DoRewrite x1 x2 -> do putWord8 5
2297+ put x1
2298+ put x2
2295 get
2299 get
2296 = do i <- getWord8
2300 = do i <- getWord8
2297 case i of
2301 case i of
@@ -2318,6 +2322,10 @@ instance (Binary t) => Binary (PDo' t) where
2318 x2 <- get
2322 x2 <- get
2319 x3 <- get
2323 x3 <- get
2320 return (DoLetP x1 x2 x3)
2324 return (DoLetP x1 x2 x3)
2325+ 5 -> do
2326+ x1 <- get
2327+ x2 <- get
2328+ return (DoRewrite x1 x2)
2321 _ -> error "Corrupted binary data for PDo'"
2329 _ -> error "Corrupted binary data for PDo'"
2322
2330
2323
2331
src/Idris/IdrisDoc.hs+2
@@ -18,6 +18,7 @@ import Idris.Core.TT (Name(..), OutputAnnotation(..), SpecialName(..),
18import Idris.Docs
18import Idris.Docs
19import Idris.Docstrings (nullDocstring)
19import Idris.Docstrings (nullDocstring)
20import qualified Idris.Docstrings as Docstrings
20import qualified Idris.Docstrings as Docstrings
21+import Idris.Options
21import Idris.Parser.Helpers (opChars)
22import Idris.Parser.Helpers (opChars)
22import IRTS.System (getIdrisDataFileByName)
23import IRTS.System (getIdrisDataFileByName)
23
24
@@ -343,6 +344,7 @@ extractPDo (DoBindP _ p1 p2 ps) = let (ps1, ps2) = unzip ps
343 in concatMap extract (p1 : p2 : ps')
344 in concatMap extract (p1 : p2 : ps')
344extractPDo (DoLet _ n _ p1 p2) = n : concatMap extract [p1, p2]
345extractPDo (DoLet _ n _ p1 p2) = n : concatMap extract [p1, p2]
345extractPDo (DoLetP _ p1 p2) = concatMap extract [p1, p2]
346extractPDo (DoLetP _ p1 p2) = concatMap extract [p1, p2]
347+extractPDo (DoRewrite _ p) = extract p
346
348
347-- | Helper function for extractPTermNames
349-- | Helper function for extractPTermNames
348extractPTactic :: PTactic -> [Name]
350extractPTactic :: PTactic -> [Name]
src/Idris/Info.hs+1−1
@@ -25,8 +25,8 @@ module Idris.Info
25 , getIdrisDataFileByName
25 , getIdrisDataFileByName
26 ) where
26 ) where
27
27
28−import Idris.AbsSyntax (loggingCatsStr)
29import Idris.Imports (installedPackages)
28import Idris.Imports (installedPackages)
29+import Idris.Options (loggingCatsStr)
30import qualified IRTS.System as S
30import qualified IRTS.System as S
31
31
32import Paths_idris
32import Paths_idris
src/Idris/Interactive.hs+14−16
@@ -37,7 +37,7 @@ import System.IO
37
37
38caseSplitAt :: FilePath -> Bool -> Int -> Name -> Idris ()
38caseSplitAt :: FilePath -> Bool -> Int -> Name -> Idris ()
39caseSplitAt fn updatefile l n
39caseSplitAt fn updatefile l n
40− = do src <- runIO $ readSource fn
40+ = do src <- runIO $ readSourceStrict fn
41 (ok, res) <- splitOnLine l n fn
41 (ok, res) <- splitOnLine l n fn
42 logLvl 1 (showSep "\n" (map show res))
42 logLvl 1 (showSep "\n" (map show res))
43 let (before, (ap : later)) = splitAt (l-1) (lines src)
43 let (before, (ap : later)) = splitAt (l-1) (lines src)
@@ -61,7 +61,7 @@ addClauseFrom fn updatefile l n = do
61 case metavars of
61 case metavars of
62 Nothing -> addMissing fn updatefile l n
62 Nothing -> addMissing fn updatefile l n
63 Just _ -> do
63 Just _ -> do
64− src <- runIO $ readSource fn
64+ src <- runIO $ readSourceStrict fn
65 let (before, tyline : later) = splitAt (l-1) (lines src)
65 let (before, tyline : later) = splitAt (l-1) (lines src)
66 let indent = getIndent 0 (show n) tyline
66 let indent = getIndent 0 (show n) tyline
67 cl <- getClause l fulln n fn
67 cl <- getClause l fulln n fn
@@ -88,7 +88,7 @@ addClauseFrom fn updatefile l n = do
88
88
89addProofClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()
89addProofClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()
90addProofClauseFrom fn updatefile l n
90addProofClauseFrom fn updatefile l n
91− = do src <- runIO $ readSource fn
91+ = do src <- runIO $ readSourceStrict fn
92 let (before, tyline : later) = splitAt (l-1) (lines src)
92 let (before, tyline : later) = splitAt (l-1) (lines src)
93 let indent = getIndent 0 (show n) tyline
93 let indent = getIndent 0 (show n) tyline
94 cl <- getProofClause l n fn
94 cl <- getProofClause l n fn
@@ -109,9 +109,9 @@ addProofClauseFrom fn updatefile l n
109
109
110addMissing :: FilePath -> Bool -> Int -> Name -> Idris ()
110addMissing :: FilePath -> Bool -> Int -> Name -> Idris ()
111addMissing fn updatefile l n
111addMissing fn updatefile l n
112− = do src <- runIO $ readSource fn
112+ = do src <- runIO $ readSourceStrict fn
113 let (before, tyline : later) = splitAt (l-1) (lines src)
113 let (before, tyline : later) = splitAt (l-1) (lines src)
114− let indent = getIndent 0 (show n) tyline
114+ let indent = getIndent tyline
115 i <- getIState
115 i <- getIState
116 cl <- getInternalApp fn l
116 cl <- getInternalApp fn l
117 let n' = getAppName cl
117 let n' = getAppName cl
@@ -124,10 +124,10 @@ addMissing fn updatefile l n
124 if updatefile
124 if updatefile
125 then do let fb = fn ++ "~"
125 then do let fb = fn ++ "~"
126 runIO $ writeSource fb (unlines (before ++ nonblank)
126 runIO $ writeSource fb (unlines (before ++ nonblank)
127− ++ extras ++
127+ ++ extras
128− (if null extras then ""
128+ ++ (if null extras then "" else "\n")
129− else "\n" ++ unlines rest))
129+ ++ unlines rest)
130− runIO $ copyFile fb fn
130+ runIO $ (length src `seq` copyFile fb fn)
131 else iPrintResult extras
131 else iPrintResult extras
132 where showPat = show . stripNS
132 where showPat = show . stripNS
133 stripNS tm = mapPT dens tm where
133 stripNS tm = mapPT dens tm where
@@ -155,14 +155,12 @@ addMissing fn updatefile l n
155 "\n" ++ rest))
155 "\n" ++ rest))
156 showNew nm i _ [] = return ""
156 showNew nm i _ [] = return ""
157
157
158− getIndent i n [] = 0
158+ getIndent s = length (takeWhile isSpace s)
159− getIndent i n xs | take (length n) xs == n = i
160− getIndent i n (x : xs) = getIndent (i + 1) n xs
161
159
162
160
163makeWith :: FilePath -> Bool -> Int -> Name -> Idris ()
161makeWith :: FilePath -> Bool -> Int -> Name -> Idris ()
164makeWith fn updatefile l n = do
162makeWith fn updatefile l n = do
165− src <- runIO $ readSource fn
163+ src <- runIO $ readSourceStrict fn
166 i <- getIState
164 i <- getIState
167 indentWith <- getIndentWith
165 indentWith <- getIndentWith
168 let (before, tyline : later) = splitAt (l-1) (lines src)
166 let (before, tyline : later) = splitAt (l-1) (lines src)
@@ -186,7 +184,7 @@ makeWith fn updatefile l n = do
186-- block, using a _ for the scrutinee
184-- block, using a _ for the scrutinee
187makeCase :: FilePath -> Bool -> Int -> Name -> Idris ()
185makeCase :: FilePath -> Bool -> Int -> Name -> Idris ()
188makeCase fn updatefile l n
186makeCase fn updatefile l n
189− = do src <- runIO $ readSource fn
187+ = do src <- runIO $ readSourceStrict fn
190 let (before, tyline : later) = splitAt (l-1) (lines src)
188 let (before, tyline : later) = splitAt (l-1) (lines src)
191 let newcase = addCaseSkel (show n) tyline
189 let newcase = addCaseSkel (show n) tyline
192
190
@@ -226,7 +224,7 @@ doProofSearch :: FilePath -> Bool -> Bool ->
226doProofSearch fn updatefile rec l n hints Nothing
224doProofSearch fn updatefile rec l n hints Nothing
227 = doProofSearch fn updatefile rec l n hints (Just 20)
225 = doProofSearch fn updatefile rec l n hints (Just 20)
228doProofSearch fn updatefile rec l n hints (Just depth)
226doProofSearch fn updatefile rec l n hints (Just depth)
229− = do src <- runIO $ readSource fn
227+ = do src <- runIO $ readSourceStrict fn
230 let (before, tyline : later) = splitAt (l-1) (lines src)
228 let (before, tyline : later) = splitAt (l-1) (lines src)
231 ctxt <- getContext
229 ctxt <- getContext
232 mn <- case lookupNames n ctxt of
230 mn <- case lookupNames n ctxt of
@@ -321,7 +319,7 @@ addBracket True new | any isSpace new = '(' : new ++ ")"
321
319
322makeLemma :: FilePath -> Bool -> Int -> Name -> Idris ()
320makeLemma :: FilePath -> Bool -> Int -> Name -> Idris ()
323makeLemma fn updatefile l n
321makeLemma fn updatefile l n
324− = do src <- runIO $ readSource fn
322+ = do src <- runIO $ readSourceStrict fn
325 let (before, tyline : later) = splitAt (l-1) (lines src)
323 let (before, tyline : later) = splitAt (l-1) (lines src)
326
324
327 -- if the name is in braces, rather than preceded by a ?, treat it
325 -- 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
22import Idris.IBC
22import Idris.IBC
23import Idris.Info
23import Idris.Info
24import Idris.ModeCommon
24import Idris.ModeCommon
25+import Idris.Options
25import Idris.Output
26import Idris.Output
26import Idris.Parser hiding (indent)
27import Idris.Parser hiding (indent)
27import Idris.REPL
28import Idris.REPL
src/Idris/ModeCommon.hs+1
@@ -15,6 +15,7 @@ import Idris.Error
15import Idris.IBC
15import Idris.IBC
16import Idris.Imports
16import Idris.Imports
17import Idris.Info
17import Idris.Info
18+import Idris.Options
18import Idris.Output
19import Idris.Output
19import Idris.Parser hiding (indent)
20import Idris.Parser hiding (indent)
20import IRTS.Exports
21import 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
6Maintainer : The Idris Community.
6Maintainer : The Idris Community.
7-}
7-}
8
8
9+{-# LANGUAGE FlexibleInstances #-}
9{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
10{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
10
11
11module Idris.Output where
12module Idris.Output where
@@ -17,6 +18,7 @@ import Idris.Core.TT
17import Idris.Delaborate
18import Idris.Delaborate
18import Idris.Docstrings
19import Idris.Docstrings
19import Idris.IdeMode
20import Idris.IdeMode
21+import Idris.Options
20
22
21import Util.Pretty
23import Util.Pretty
22import Util.ScreenSize (getScreenWidth)
24import Util.ScreenSize (getScreenWidth)
src/Idris/Package.hs+1−1
@@ -35,7 +35,7 @@ import Idris.IBC
35import Idris.IdrisDoc
35import Idris.IdrisDoc
36import Idris.Imports
36import Idris.Imports
37import Idris.Main (idris, idrisMain)
37import Idris.Main (idris, idrisMain)
38−import Idris.Output (pshow)
38+import Idris.Options
39import Idris.Output
39import Idris.Output
40import Idris.Parser (loadModule)
40import Idris.Parser (loadModule)
41import Idris.REPL
41import Idris.REPL
src/Idris/Package/Common.hs+1−1
@@ -6,8 +6,8 @@ Maintainer : The Idris Community.
6-}
6-}
7module Idris.Package.Common where
7module Idris.Package.Common where
8
8
9−import Idris.AbsSyntaxTree (Opt(..))
10import Idris.Core.TT (Name)
9import Idris.Core.TT (Name)
10+import Idris.Options (Opt(..))
11
11
12-- | Description of an Idris package.
12-- | Description of an Idris package.
13data PkgDesc = PkgDesc {
13data PkgDesc = PkgDesc {
src/Idris/Package/Parser.hs+17−13
@@ -5,10 +5,7 @@ Copyright :
5License : BSD3
5License : BSD3
6Maintainer : The Idris Community.
6Maintainer : The Idris Community.
7-}
7-}
8−{-# LANGUAGE CPP, ConstraintKinds #-}
8+{-# LANGUAGE CPP, ConstraintKinds, FlexibleInstances, TypeSynonymInstances #-}
9−#if !(MIN_VERSION_base(4,8,0))
10−{-# LANGUAGE OverlappingInstances #-}
11−#endif
12module Idris.Package.Parser where
9module Idris.Package.Parser where
13
10
14import Idris.AbsSyntaxTree
11import Idris.AbsSyntaxTree
@@ -24,7 +21,9 @@ import Control.Applicative
24import Control.Monad.State.Strict
21import Control.Monad.State.Strict
25import Data.List (union)
22import Data.List (union)
26import Data.Maybe (fromJust, isNothing)
23import Data.Maybe (fromJust, isNothing)
24+import System.Directory (doesFileExist)
25+import System.Exit
27−import System.FilePath (isValid, takeFileName)
26+import System.FilePath (isValid, takeExtension, takeFileName)
28import qualified Text.PrettyPrint.ANSI.Leijen as PP
27import qualified Text.PrettyPrint.ANSI.Leijen as PP
29import Text.Trifecta hiding (char, charLiteral, natural, span, string, symbol,
28import Text.Trifecta hiding (char, charLiteral, natural, span, string, symbol,
30 whiteSpace)
29 whiteSpace)
@@ -48,20 +47,25 @@ instance {-# OVERLAPPING #-} DeltaParsing PParser where
48 {-# INLINE restOfLine #-}
47 {-# INLINE restOfLine #-}
49#endif
48#endif
50
49
51−#if MIN_VERSION_base(4,8,0)
52instance {-# OVERLAPPING #-} TokenParsing PParser where
50instance {-# OVERLAPPING #-} TokenParsing PParser where
53−#else
54−instance TokenParsing PParser where
55−#endif
56 someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()
51 someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()
57
52
58
53
59parseDesc :: FilePath -> IO PkgDesc
54parseDesc :: FilePath -> IO PkgDesc
60parseDesc fp = do
55parseDesc fp = do
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
61− p <- readFile fp
62+ p <- readFile fp
62− case runparser pPkg defaultPkg fp p of
63+ case runparser pPkg defaultPkg fp p of
63− Failure (ErrInfo err _) -> fail (show $ PP.plain err)
64+ Failure (ErrInfo err _) -> fail (show $ PP.plain err)
64− Success x -> return x
65+ Success x -> return x
66+ else do
67+ putStrLn $ unwords [ "The presented iPKG file does not exist:", show fp]
68+ exitWith (ExitFailure 1)
65
69
66pPkg :: PParser PkgDesc
70pPkg :: PParser PkgDesc
67pPkg = do
71pPkg = do
src/Idris/Parser.hs+8−2
@@ -5,7 +5,8 @@ Copyright :
5License : BSD3
5License : BSD3
6Maintainer : The Idris Community.
6Maintainer : The Idris Community.
7-}
7-}
8−{-# LANGUAGE ConstraintKinds, GeneralizedNewtypeDeriving, PatternGuards #-}
8+{-# LANGUAGE ConstraintKinds, FlexibleContexts, GeneralizedNewtypeDeriving,
9+ PatternGuards #-}
9{-# OPTIONS_GHC -O0 #-}
10{-# OPTIONS_GHC -O0 #-}
10module Idris.Parser(module Idris.Parser,
11module Idris.Parser(module Idris.Parser,
11 module Idris.Parser.Expr,
12 module Idris.Parser.Expr,
@@ -26,6 +27,7 @@ import Idris.ElabDecls
26import Idris.Error
27import Idris.Error
27import Idris.IBC
28import Idris.IBC
28import Idris.Imports
29import Idris.Imports
30+import Idris.Options
29import Idris.Output
31import Idris.Output
30import Idris.Parser.Data
32import Idris.Parser.Data
31import Idris.Parser.Expr
33import Idris.Parser.Expr
@@ -1568,7 +1570,8 @@ parseImports fname input
1568 [ImportInfo],
1570 [ImportInfo],
1569 Maybe Delta),
1571 Maybe Delta),
1570 [(FC, OutputAnnotation)], IState)
1572 [(FC, OutputAnnotation)], IState)
1573+ imports = do optional shebang
1571− imports = do whiteSpace
1574+ whiteSpace
1572 (mdoc, mname, annots) <- moduleHeader
1575 (mdoc, mname, annots) <- moduleHeader
1573 ps_exp <- many import_
1576 ps_exp <- many import_
1574 mrk <- mark
1577 mrk <- mark
@@ -1593,6 +1596,9 @@ parseImports fname input
1593 (fc, AnnNamespace ns (Just path)) : addPath annots path
1596 (fc, AnnNamespace ns (Just path)) : addPath annots path
1594 addPath (annot:annots) path = annot : addPath annots path
1597 addPath (annot:annots) path = annot : addPath annots path
1595
1598
1599+ shebang :: IdrisParser ()
1600+ shebang = string "#!" *> many (satisfy $ not . isEol) *> eol *> pure ()
1601+
1596-- | There should be a better way of doing this...
1602-- | There should be a better way of doing this...
1597findFC :: Doc -> (FC, String)
1603findFC :: Doc -> (FC, String)
1598findFC x = let s = show (plain x) in findFC' s
1604findFC x = let s = show (plain x) in findFC' s
src/Idris/Parser/Data.hs+1
@@ -13,6 +13,7 @@ import Idris.Core.Evaluate
13import Idris.Core.TT
13import Idris.Core.TT
14import Idris.Docstrings
14import Idris.Docstrings
15import Idris.DSL
15import Idris.DSL
16+import Idris.Options
16import Idris.Parser.Expr
17import Idris.Parser.Expr
17import Idris.Parser.Helpers
18import Idris.Parser.Helpers
18import Idris.Parser.Ops
19import Idris.Parser.Ops
src/Idris/Parser/Expr.hs+8
@@ -12,6 +12,7 @@ module Idris.Parser.Expr where
12import Idris.AbsSyntax
12import Idris.AbsSyntax
13import Idris.Core.TT
13import Idris.Core.TT
14import Idris.DSL
14import Idris.DSL
15+import Idris.Options
15import Idris.Parser.Helpers
16import Idris.Parser.Helpers
16import Idris.Parser.Ops
17import Idris.Parser.Ops
17
18
@@ -233,6 +234,7 @@ updateSynMatch = update
233 = DoBindP fc (update ns i) (update ns t)
234 = DoBindP fc (update ns i) (update ns t)
234 (map (\(l,r) -> (update ns l, update ns r)) ts)
235 (map (\(l,r) -> (update ns l, update ns r)) ts)
235 upd ns (DoLetP fc i t) = DoLetP fc (update ns i) (update ns t)
236 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)
236 update ns (PIdiom fc t) = PIdiom fc $ update ns t
238 update ns (PIdiom fc t) = PIdiom fc $ update ns t
237 update ns (PMetavar fc n) = uncurry (flip PMetavar) $ updateB ns (n, fc)
239 update ns (PMetavar fc n) = uncurry (flip PMetavar) $ updateB ns (n, fc)
238 update ns (PProof tacs) = PProof $ map (updTactic ns) tacs
240 update ns (PProof tacs) = PProof $ map (updTactic ns) tacs
@@ -1342,6 +1344,7 @@ doBlock syn
1342Do ::=
1344Do ::=
1343 'let' Name TypeSig'? '=' Expr
1345 'let' Name TypeSig'? '=' Expr
1344 | 'let' Expr' '=' Expr
1346 | 'let' Expr' '=' Expr
1347+ | 'rewrite Expr
1345 | Name '<-' Expr
1348 | Name '<-' Expr
1346 | Expr' '<-' Expr
1349 | Expr' '<-' Expr
1347 | Expr
1350 | Expr
@@ -1366,6 +1369,11 @@ do_ syn
1366 sc <- expr syn
1369 sc <- expr syn
1367 highlightP kw AnnKeyword
1370 highlightP kw AnnKeyword
1368 return (DoLetP fc i sc))
1371 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))
1369 <|> try (do (i, ifc) <- name
1377 <|> try (do (i, ifc) <- name
1370 symbol "<-"
1378 symbol "<-"
1371 fc <- getFC
1379 fc <- getFC
src/Idris/Parser/Helpers.hs+4−9
@@ -5,11 +5,9 @@ Copyright :
5License : BSD3
5License : BSD3
6Maintainer : The Idris Community.
6Maintainer : The Idris Community.
7-}
7-}
8+{-# LANGUAGE CPP, ConstraintKinds, FlexibleInstances,
8−{-# LANGUAGE CPP, ConstraintKinds, GeneralizedNewtypeDeriving, PatternGuards,
9+ GeneralizedNewtypeDeriving, PatternGuards, StandaloneDeriving,
9− StandaloneDeriving #-}
10+ TypeSynonymInstances #-}
10−#if !(MIN_VERSION_base(4,8,0))
11−{-# LANGUAGE OverlappingInstances #-}
12−#endif
13module Idris.Parser.Helpers where
11module Idris.Parser.Helpers where
14
12
15import Idris.AbsSyntax
13import Idris.AbsSyntax
@@ -17,6 +15,7 @@ import Idris.Core.Evaluate
17import Idris.Core.TT
15import Idris.Core.TT
18import Idris.Delaborate (pprintErr)
16import Idris.Delaborate (pprintErr)
19import Idris.Docstrings
17import Idris.Docstrings
18+import Idris.Options
20import Idris.Output (iWarn)
19import Idris.Output (iWarn)
21
20
22import qualified Util.Pretty as Pretty (text)
21import qualified Util.Pretty as Pretty (text)
@@ -69,11 +68,7 @@ instance {-# OVERLAPPING #-} DeltaParsing IdrisParser where
69
68
70#endif
69#endif
71
70
72−#if MIN_VERSION_base(4,8,0)
73instance {-# OVERLAPPING #-} TokenParsing IdrisParser where
71instance {-# OVERLAPPING #-} TokenParsing IdrisParser where
74−#else
75−instance TokenParsing IdrisParser where
76−#endif
77 someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()
72 someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()
78 token p = do s <- get
73 token p = do s <- get
79 (FC fn (sl, sc) _) <- getFC --TODO: Update after fixing getFC
74 (FC fn (sl, sc) _) <- getFC --TODO: Update after fixing getFC
src/Idris/Parser/Ops.hs+2−1
@@ -5,7 +5,8 @@ Copyright :
5License : BSD3
5License : BSD3
6Maintainer : The Idris Community.
6Maintainer : The Idris Community.
7-}
7-}
8−{-# LANGUAGE ConstraintKinds, GeneralizedNewtypeDeriving, PatternGuards #-}
8+{-# LANGUAGE ConstraintKinds, FlexibleContexts, GeneralizedNewtypeDeriving,
9+ PatternGuards #-}
9module Idris.Parser.Ops where
10module Idris.Parser.Ops where
10
11
11import Idris.AbsSyntax
12import Idris.AbsSyntax
src/Idris/PartialEval.hs+1−1
@@ -5,7 +5,7 @@ Copyright :
5License : BSD3
5License : BSD3
6Maintainer : The Idris Community.
6Maintainer : The Idris Community.
7-}
7-}
8−{-# LANGUAGE PatternGuards #-}
8+{-# LANGUAGE FlexibleContexts, PatternGuards #-}
9
9
10module Idris.PartialEval(
10module Idris.PartialEval(
11 partial_eval, getSpecApps, specType
11 partial_eval, getSpecApps, specType
src/Idris/Prover.hs+2
@@ -32,6 +32,7 @@ import Idris.Elab.Value
32import Idris.ElabDecls
32import Idris.ElabDecls
33import Idris.Error
33import Idris.Error
34import qualified Idris.IdeMode as IdeMode
34import qualified Idris.IdeMode as IdeMode
35+import Idris.Options
35import Idris.Output
36import Idris.Output
36import Idris.Parser hiding (params)
37import Idris.Parser hiding (params)
37import Idris.TypeSearch (searchByType)
38import Idris.TypeSearch (searchByType)
@@ -349,6 +350,7 @@ elabloop info fn d prompt prf e prev h env
349 Success (Right cmd') ->
350 Success (Right cmd') ->
350 case cmd' of
351 case cmd' of
351 DoLetP {} -> ifail "Pattern-matching let not supported here"
352 DoLetP {} -> ifail "Pattern-matching let not supported here"
353+ DoRewrite {} -> ifail "Pattern-matching do-rewrite not supported here"
352 DoBindP {} -> ifail "Pattern-matching <- not supported here"
354 DoBindP {} -> ifail "Pattern-matching <- not supported here"
353 DoLet fc i ifc Placeholder expr ->
355 DoLet fc i ifc Placeholder expr ->
354 do (tm, ty) <- elabVal (recinfo proverfc) ERHS (inLets ist env expr)
356 do (tm, ty) <- elabVal (recinfo proverfc) ERHS (inLets ist env expr)
src/Idris/REPL.hs+2−1
@@ -5,7 +5,7 @@ License : BSD3
5Maintainer : The Idris Community.
5Maintainer : The Idris Community.
6-}
6-}
7
7
8−{-# LANGUAGE PatternGuards #-}
8+{-# LANGUAGE FlexibleContexts, PatternGuards #-}
9
9
10module Idris.REPL
10module Idris.REPL
11 ( idemodeStart
11 ( idemodeStart
@@ -68,6 +68,7 @@ import Idris.Info
68import Idris.Inliner
68import Idris.Inliner
69import Idris.Interactive
69import Idris.Interactive
70import Idris.ModeCommon
70import Idris.ModeCommon
71+import Idris.Options
71import Idris.Output
72import Idris.Output
72import Idris.Parser hiding (indent)
73import Idris.Parser hiding (indent)
73import Idris.Prover
74import Idris.Prover
src/Idris/REPL/Commands.hs+1
@@ -3,6 +3,7 @@ module Idris.REPL.Commands where
3import Idris.AbsSyntaxTree
3import Idris.AbsSyntaxTree
4import Idris.Colours
4import Idris.Colours
5import Idris.Core.TT
5import Idris.Core.TT
6+import Idris.Options
6
7
7-- | REPL commands
8-- | REPL commands
8data Command = Quit
9data Command = Quit
src/Idris/REPL/Parser.hs+1
@@ -15,6 +15,7 @@ import Idris.AbsSyntax
15import Idris.Colours
15import Idris.Colours
16import Idris.Core.TT
16import Idris.Core.TT
17import Idris.Help
17import Idris.Help
18+import Idris.Options
18import qualified Idris.Parser as P
19import qualified Idris.Parser as P
19import Idris.REPL.Commands
20import Idris.REPL.Commands
20
21
src/Idris/Reflection.hs−5
@@ -21,11 +21,6 @@ import Idris.AbsSyntaxTree (ArgOpt(..), ElabD, Fixity(..), IState(idris_datatype
21 initEState, pairCon, pairTy)
21 initEState, pairCon, pairTy)
22import Idris.Delaborate (delab)
22import Idris.Delaborate (delab)
23
23
24−#if __GLASGOW_HASKELL__ < 710
25−import Control.Applicative (pure, (<$>), (<*>))
26−import Data.Traversable (mapM)
27−import Prelude hiding (mapM)
28−#endif
29import Control.Monad (liftM, liftM2, liftM4)
24import Control.Monad (liftM, liftM2, liftM4)
30import Control.Monad.State.Strict (lift)
25import Control.Monad.State.Strict (lift)
31import Data.List (findIndex, (\\))
26import Data.List (findIndex, (\\))
src/Idris/Termination.hs+1
@@ -14,6 +14,7 @@ import Idris.Core.Evaluate
14import Idris.Core.TT
14import Idris.Core.TT
15import Idris.Delaborate
15import Idris.Delaborate
16import Idris.Error
16import Idris.Error
17+import Idris.Options
17import Idris.Output (iWarn, iputStrLn)
18import Idris.Output (iWarn, iputStrLn)
18
19
19import Control.Monad.State.Strict
20import Control.Monad.State.Strict
src/Util/Pretty.hs+3
@@ -5,6 +5,9 @@ Copyright :
5License : BSD3
5License : BSD3
6Maintainer : The Idris Community.
6Maintainer : The Idris Community.
7-}
7-}
8+
9+{-# LANGUAGE MultiParamTypeClasses #-}
10+
8module Util.Pretty (
11module Util.Pretty (
9 module Text.PrettyPrint.Annotated.Leijen
12 module Text.PrettyPrint.Annotated.Leijen
10 , Sized(..)
13 , Sized(..)
src/Util/System.hs+10
@@ -14,6 +14,7 @@ module Util.System( tempfile
14 , writeSource
14 , writeSource
15 , writeSourceText
15 , writeSourceText
16 , readSource
16 , readSource
17+ , readSourceStrict
17 , setupBundledCC
18 , setupBundledCC
18 , isATTY
19 , isATTY
19 ) where
20 ) where
@@ -60,6 +61,15 @@ readSource f = do h <- openFile f ReadMode
60 hSetEncoding h utf8
61 hSetEncoding h utf8
61 hGetContents h
62 hGetContents h
62
63
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+
63-- | Write a source file, same as writeFile except the encoding is set to utf-8
73-- | Write a source file, same as writeFile except the encoding is set to utf-8
64writeSource :: FilePath -> String -> IO ()
74writeSource :: FilePath -> String -> IO ()
65writeSource f s = withFile f WriteMode (\h -> hSetEncoding h utf8 >> hPutStr h s)
75writeSource f s = withFile f WriteMode (\h -> hSetEncoding h utf8 >> hPutStr h s)
stack-shell.nix+1−1
@@ -2,7 +2,7 @@ with (import <nixpkgs> {});
2
2
3let
3let
4 # MUST match resolver in stack.yaml
4 # MUST match resolver in stack.yaml
5− resolver = haskell.packages.lts-8_06.ghc;
5+ resolver = haskell.packages.lts-9_0.ghc;
6
6
7 native_libs = [
7 native_libs = [
8 libffi
8 libffi
stack.yaml+1−1
@@ -1,4 +1,4 @@
1−resolver: lts-8.06
1+resolver: lts-9.0
2
2
3packages:
3packages:
4 - location: .
4 - location: .
test/TestData.hs+5−2
@@ -155,7 +155,9 @@ testFamiliesData = [
155 ( 11, ANY ),
155 ( 11, ANY ),
156 ( 12, ANY ),
156 ( 12, ANY ),
157 ( 13, ANY ),
157 ( 13, ANY ),
158− ( 14, C_CG )]),
158+ ( 14, C_CG ),
159+ ( 15, ANY ),
160+ ( 16, ANY )]),
159 ("interfaces", "Interfaces",
161 ("interfaces", "Interfaces",
160 [ ( 1, ANY ),
162 [ ( 1, ANY ),
161 ( 2, ANY ),
163 ( 2, ANY ),
@@ -256,7 +258,8 @@ testFamiliesData = [
256 ( 77, ANY )]),
258 ( 77, ANY )]),
257 ("regression", "Regression",
259 ("regression", "Regression",
258 [ ( 1 , ANY ),
260 [ ( 1 , ANY ),
259− ( 2 , ANY )]),
261+ ( 2 , ANY ),
262+ ( 3 , ANY )]),
260 ("sourceLocation", "Source location",
263 ("sourceLocation", "Source location",
261 [ ( 1 , ANY )]),
264 [ ( 1 , ANY )]),
262 ("sugar", "Syntactic sugar",
265 ("sugar", "Syntactic sugar",
test/TestRun.hs−2
@@ -7,9 +7,7 @@ import Control.Monad
7import Data.Char (isLetter)
7import Data.Char (isLetter)
8import qualified Data.IntMap as IMap
8import qualified Data.IntMap as IMap
9import Data.List
9import Data.List
10−#if MIN_VERSION_optparse_applicative(0,13,0)
11import Data.Monoid ((<>))
10import Data.Monoid ((<>))
12−#endif
13import Data.Proxy
11import Data.Proxy
14import Data.Typeable
12import Data.Typeable
15import Options.Applicative
13import Options.Applicative
test/basic009/expected+1−1
@@ -1,5 +1,5 @@
1MAIN-PASS
1MAIN-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
3 Did you mean to refer to A.num?
3 Did you mean to refer to A.num?
4Faulty.idr:7:7:When checking right hand side of fault with expected type
4Faulty.idr:7:7:When checking right hand side of fault with expected type
5 num = 0
5 num = 0
test/basic018/expected+4−2
@@ -1,6 +1,8 @@
1+basic018.idr:7:12-17:
1−basic018.idr:7:12-17:WARNING: thing is bound as an implicit
2+thing is bound as an implicit
2 Did you mean to refer to Main.thing?
3 Did you mean to refer to Main.thing?
4+basic018.idr:12:8-13:
3−basic018.idr:12:8-13:WARNING: thing is bound as an implicit
5+thing is bound as an implicit
4 Did you mean to refer to Main.thing?
6 Did you mean to refer to Main.thing?
5basic018.idr:13:6:When checking right hand side of test with expected type
7basic018.idr:13:6:When checking right hand side of test with expected type
6 thing = S 41
8 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
18Elaborating type decl Main.main[]
18Elaborating type decl Main.main[]
19Elaborating clause Main.main
19Elaborating clause Main.main
20Rechecking for positivity []
20Rechecking 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
3rm -f *.ibc
3rm -f *.ibc
4${IDRIS:-idris} $@ --build test-pkg.ipkg --quiet
4${IDRIS:-idris} $@ --build test-pkg.ipkg --quiet
5${IDRIS:-idris} $@ --build test-pkg.ipkg --logging-categories "elab" --log 1
5${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))
10
10
11 data Elem : a -> List a -> Type where
11 data Elem : a -> List a -> Type where
12 Stop : Elem x (x :: xs)
12 Stop : Elem x (x :: xs)
13− Pop : Elem x ys -> Elem x (y :: xs)
13+ Pop : Elem x ys -> Elem x (y :: ys)
14
14
15-- Expr is a reflection of a list, indexed over the concrete list,
15-- Expr is a reflection of a list, indexed over the concrete list,
16-- and over a set of list variables.
16-- 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.
110This is likely to lead to problems!
110This is likely to lead to problems!
111reg068.idr:2:6:Main.ze has a name which may be implicitly bound.
111reg068.idr:2:6:Main.ze has a name which may be implicitly bound.
112This is likely to lead to problems!
112This is likely to lead to problems!
113+reg068.idr:2:8-11:
113−reg068.idr:2:8-11:WARNING: nat is bound as an implicit
114+nat is bound as an implicit
114 Did you mean to refer to Main.nat?
115 Did you mean to refer to Main.nat?
115reg068.idr:2:6:When checking constructor Main.ze:
116reg068.idr:2:6:When checking constructor Main.ze:
116Type level variable nat is not Main.nat
117Type 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