Commit Graph

364 Commits

Author SHA1 Message Date
Thomas Herzog
e39477aa0e added more functions to Control.App.Console
Now all common console IO functions available from the
prelude are available through the `Control.App.Console`
interface.

Added:
- putChar
- getChar
- getCharLn
- print
- printLn

Renamed:
- getStr to getLine
2020-05-30 12:44:40 +02:00
Edwin Brady
843b30b4d1
Merge pull request #196 from edwinb/with-experiment
Experiment %syntactic flag on with
2020-05-29 17:01:41 +01:00
Edwin Brady
d869eb666c Experiment %syntactic flag on with
This means it abstracts over the value syntactically, rather than by
value, and can significantly speed up elaboration where large types are
involved, at a cost of being less general. Try it if "with" is slow.

There are more flags we want on with (well, at least one: "proof")
2020-05-29 16:39:11 +01:00
Fabián Heredia Montiel
0537aa12f5 Let DocComments trough from Lexer to Parser 2020-05-29 10:37:04 +01:00
Edwin Brady
1d87e3cd18
Merge pull request #192 from edwinb/as-patterns
As patterns
2020-05-28 19:46:31 +01:00
Edwin Brady
3b5f47d922 As patterns fix
As patterns weren't getting propagated to local definitions, due to a
combination of being stored as let bindings and being part of a pattern
scrutinee. The solution removes the computation behaviour, but that is
consistent with the way let works everywhere else.

(If we do as patterns as let bindings, the way case and locals elaborate
mean that the value gets recomputed. Fixing this would require changing
the way the core works, and I'm not going to do that for a while.)
2020-05-28 18:57:06 +01:00
Edwin Brady
aad56c723f
Merge pull request #191 from edwinb/totality
Totality checking
2020-05-28 16:28:06 +01:00
Edwin Brady
fdda6b1a70 Merge https://github.com/idris-lang/Idris2 2020-05-28 16:16:23 +01:00
Niklas Larsson
40614638b7
Merge pull request #121 from timsueberkrueb/add-popen-pclose
Add popen and pclose from Idris 1
2020-05-28 17:13:26 +02:00
Edwin Brady
8c5d5055fa Update scheme
Changing the prelude totality default means we need to update the scheme
to be able to cope with its new meaning
2020-05-28 16:05:08 +01:00
Edwin Brady
4ae01d7264 %default doesn't affect interface methods
The required totality of interface methods is now only affected if
there's an explicit modifier on the method. This allows us to set
%default total on the Prelude, which is a good thing to do anyway,
without also requiring that every implementation of the interface in the
prelude has to be total, which would potentially be a pain.

Another good affect is that it speeds up totality checking elsewhere
because totality checking is done lazily, and so with the total flag set
we know in advance that prelude functions are total.
2020-05-28 15:52:03 +01:00
Tim Süberkrüb
42a1522a3b Try to make Windows happy with backslashes 2020-05-28 16:42:56 +02:00
Edwin Brady
2223d50c3a Skip totality check on case blocks and MNs
These are checked as part of checking the top level names
2020-05-28 15:32:46 +01:00
Edwin Brady
674027f7ce Termination checking performance improvement
Remove duplicates from the size change graph, and cut short the search
on encountering a name with an already known termination status.
2020-05-28 15:17:22 +01:00
Fabián Heredia Montiel
97366f022d Add missing totality annotations 2020-05-28 15:17:14 +01:00
Tim Süberkrüb
46f7b78b0e Try to fix pclose for Windows
Co-authored-by: Niklas Larsson <metaniklas@gmail.com>
2020-05-28 16:12:26 +02:00
Fabián Heredia Montiel
fd58d25783 Remove unused imports from Idris.Main 2020-05-28 14:56:28 +01:00
Edwin Brady
684c5037ae
Merge pull request #190 from edwinb/various-fixes
Various fixes
2020-05-28 13:18:21 +01:00
Edwin Brady
6ffe4c5257 Don't write metavariable types to ttc!
On second thoughts, and after further experimentation, better to recheck
the metavariable if it arises in linearity checking, because the type
could be very big and in general will be much bigger than the
definition. If this turns out to be a performance issue later, we can
revisit it.
2020-05-28 12:42:38 +01:00
Edwin Brady
00d6027b75 Unset tcinline flag after checking interface
In this case, it's only needed to ensure the dictionaries are inlined
when checking recursive methods, so can be unset once we're done, to
save excessive inlining when totality checking later.
2020-05-28 12:38:49 +01:00
Edwin Brady
a4671bae30 Save metavariable types in ttc
It's a small performance hit, but not as big as it used to be because we
don't load everything any more. This is necessary because saved
metavariables might turn up during evaluation, and then be needed in the
final linearity check. Another way is to check them again if this
happens, but there's a risk that might be even more expensive (and
saving the type is much safter anyway).
2020-05-28 12:00:39 +01:00
Tim Süberkrüb
c2dfe7de7f Add popen and pclose from Idris 1 2020-05-28 12:58:03 +02:00
Edwin Brady
dddd95e5da
Merge pull request #182 from edwinb/hash-public-import
Fix hash generation of public imports
2020-05-27 22:51:57 +01:00
Edwin Brady
315f8bff54 Fix hash generation of public imports
public imports need to change the present modules hash, but we were
updating before initialising the hash, so they never got included. Oops!
2020-05-27 22:25:40 +01:00
Niklas Larsson
4ef0cb2c15
Merge pull request #176 from MilanKral/https
replace HTTP links with HTTPS
2020-05-27 23:23:29 +02:00
Edwin Brady
2e68193d0f
Merge pull request #181 from edwinb/fix-imports
Add missing import
2020-05-27 22:20:45 +01:00
Edwin Brady
c3ed22c82f
Merge pull request #165 from stephen-smith/docs-updates
Documentation Updates based on my first experiences with Idris 2
2020-05-27 22:06:53 +01:00
Edwin Brady
1c889ec99e Add missing import
This wouldn't have got caught since the merge that caused the problem
was checked before I pushed the patch that made import work right! So
hopefully this'll sort it.
2020-05-27 21:44:37 +01:00
Edwin Brady
6b8324db3b
Merge pull request #178 from edwinb/performance
Performance
2020-05-27 21:34:11 +01:00
Niklas Larsson
696db7f58f
Merge pull request #169 from andylokandy/pathcom
Use Path in the compiler
2020-05-27 21:23:29 +02:00
Edwin Brady
70b41ca5f8 Some small parser improvements
- %inline in a few places, which helps especially when it's known at
compile time whether something consumes
- a little bit of reordering so that the most likely alternative is
tried first
- (not really much effect, but...) use fastPack from the Prelude for
building tokens
2020-05-27 19:00:33 +01:00
Boyd Stephen Smith Jr
38876800ca Mention %access specifically
(The first failure I got when trying to compile Idris 1.3.1 code with
Idris2.)
2020-05-27 12:51:41 -05:00
Edwin Brady
9129df359f Simplify doParse
If we're going to use assert_total. we might as well not have the
distinction between empty and non empty results, which only makes the
code harder to follow.

Also there's some kind of issue which seems to mean the token list can't
be erased if we do that. I will investigate if I can make a smaller
example.
2020-05-27 18:16:54 +01:00
Edwin Brady
1d078f7888
Merge pull request #177 from edwinb/fix-imports
Fix import loading
2020-05-27 16:37:57 +01:00
Edwin Brady
c88bf7af8d Fix import loading
This was taking too long, and adding too many things, because it was
going too deep in the name of having everything accessible at the REPL
and for the compiler. So, it's done a bit differently now, only chasing
everything on a "full" load (i.e., final load at the REPL)

This has some effects:
+ As systems get bigger, load time gets better (on my machine, checking
  Idris.Main now takes 52s from scratch, down from 76s)
+ You might find import errors that you didn't previously get, because
  things were being imported that shouldn't have been. The new way is
  correct!

An unfortunate effect is that sometimes you end up getting "undefined
name" errors even if you didn't explicitly use the name, because
sometimes a module uses a name from another module in a type, which then
gets exported, and eventually needs to be reduced. This mostly happens
because there is a compile time check that should be done which I
haven't implemented yet. That is, public export definitions should only
be allowed to use names that are also public export. I'll get to this
soon.
2020-05-27 15:49:03 +01:00
Milan Kral
9f78f1cddc
replace HTTP links with HTTPS 2020-05-27 14:50:05 +02:00
andylokandy
55f07485ae Fix mkdirAll 2020-05-27 18:44:33 +08:00
andylokandy
16da913441 Update doc 2020-05-27 18:32:17 +08:00
andylokandy
e8b1d54e0a Refactor Core.Directory 2020-05-27 18:21:40 +08:00
andylokandy
40401b53ec Remove the duplicate isWindows 2020-05-27 03:12:54 +08:00
Jan de Muijnck-Hughes
8b062f47cc Allow cli given option overriding for ipkg cmds.
As it was in Idris1 being able to override some, or introduce new, options to an Idris IPKG is beneficial. For example, generate code for multiple codegens from a single source.

Overridable options are:

+ `--quiet`
+ `--verbose`
+ `--timing`
+ `--dumpcases <file>`
+ `--dumplifted <file>`
+ `--dumpvmcode <file>`
+ `--debug-elab-check`
2020-05-26 14:41:09 +01:00
Jan de Muijnck-Hughes
54fd78a956 Fixed fragility of ipkg file parsing.
+ Explicitly check if an IPKG has the correct suffix.
+ Add missing case that could return a malformed error message.
2020-05-26 14:41:09 +01:00
Jan de Muijnck-Hughes
1948bfcfc6 Added 'REPL' as a command line option so the code can be used. 2020-05-26 14:41:09 +01:00
Jan de Muijnck-Hughes
68a4ad2e1c New test for detecting overridable options for IPKG commands. 2020-05-26 14:41:09 +01:00
Niklas Larsson
c23958bf16
Merge pull request #167 from ska80/sync-idris2api
Sync idris2api.ipkg with idris2.ipkg
2020-05-26 13:58:24 +02:00
andylokandy
712a4df140 Gather the straw isWindowss 2020-05-26 17:59:14 +08:00
andylokandy
fa902932fc Use Path in compiler 2020-05-26 17:43:27 +08:00
asdfjasdf
6d36b04c72 Possible copy-paste mistake in typesfuns.rst
In the intial code listing we currently have "x = 42" but in following listing "x == 9 * 9 + 13" returns true.
2020-05-26 10:21:58 +01:00
Kamil Shakirov
d5743911fe Sync idris2api.ipkg with idris2.ipkg 2020-05-26 12:24:42 +06:00
Boyd Stephen Smith Jr
7e23c844a8 Mention make install
README.md has that step, but this section of the documentation was
missing it.
2020-05-25 21:32:33 -05:00