Commit Graph

359 Commits

Author SHA1 Message Date
Denis Buzdalov
ab3862798b [ fix ] Use right reflection constructor name for unambiguing with 2021-11-23 16:42:51 +00:00
claymager
283f9bd00f
[ fix ] Forbid "." as namespace identifier (#2134) 2021-11-22 12:13:08 +00:00
Guillaume ALLAIS
0bc18bd34a [ fix #2072 ] correctly handle fixity in printer 2021-11-19 17:42:07 +00:00
Guillaume ALLAIS
f99b875d7e [ fix #2095 ] error on duplicated updates 2021-11-19 16:30:35 +00:00
Mathew Polzin
0eba4c691e
Add %deprecate pragma (#2086) 2021-11-17 10:41:03 +00:00
Zoe Stafford
3063218d46
[ new ] Add %nomangle (#2063)
This is (for once) not a breaking changes, instead backends will need to opt in to this change, using the utilities in Compiler.NoMangle. See the js backend for an example of how to do this.

This is the first step to being able to use idris to create libraries usable by other languages.
2021-11-09 16:23:50 +00:00
Edwin Brady
2f6ec76223
Get information about names in reflection (#2110)
* Only normalise a search goal if it's fast

While we do end up normalising it anyway on success, there might be
things blocking it that make the intermediate terms very big, so only do
it speculatively to see if it's quick.

* Get information about names in reflection

Currently this is only whether it's a function, or data or type
constructor. I expect more may be useful/possible.
2021-11-07 15:06:53 +00:00
Guillaume ALLAIS
a8d5e005e1 [ fix #2070 ] Look under MaybeMispelling when failing quickly 2021-10-29 17:57:55 +01:00
G. Allais
ac7a4644b8
[ fix #2046 ] only refold positive integers as nats (#2064) 2021-10-26 17:16:31 +01:00
Ellis Kesterton
9c2ce646f9
[ fix #2002 ] implicits used in record update (#2007) 2021-10-26 17:15:29 +01:00
CodingCellist
4a1bb310a7
[ fix #1175 ] case-splitting for inline case blocks (#2010) 2021-10-26 15:51:52 +01:00
Alissa Tung
1bd81dfbbb
[ fix #2053 ] do not show ambiguous private names (#2056)
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-10-26 15:51:34 +01:00
G. Allais
b9834978cb
[ re #2041 ] better runtime error for holey expression (#2045) 2021-10-26 12:43:39 +01:00
Giuseppe Lomurno
7f63a0103f Add user hints to expression search 2021-10-24 10:24:22 +01:00
Guillaume ALLAIS
8fde63396e [ fix #1626 ] Empty lines are still lines 2021-10-21 16:00:50 +01:00
Daniel Kröni
aa107a9754
Implemented %noinline (#2027)
* Implemented %noinline

* Removed trailing spaces.

* Added missing case in Reify FnOpt

* Added error message when both %inline and %noinline are set.

* Added test.

* Changed from perror to error
2021-10-19 15:22:36 +01:00
Edwin Brady
75716cd0d1
Fix casts in scheme evaluator (#2011)
* Fix casts in scheme evaluator

We really need test cases for all the primitives before we can use this
evaluator properly. Also test cases that run inside an environment,
which are a bit harder to construct.

* Add the cast fixes to racket support code

* More racket compile time evaluation fixes

We had the chez version of some primtives in the ct-support file. We
need a full set of tests for the primitives here too...
2021-10-16 14:19:26 +01:00
Edwin Brady
cfb7395eac
Add try primitive to reflection library (#2008) 2021-10-16 11:24:12 +01:00
stefan-hoeck
62237f74ea [ fix ] fastConcat for JS backends 2021-10-14 14:58:51 +01:00
G. Allais
00ab9573a5
[ re #1944 ] Allow toplevel aliases (#1952)
* [ re #1944 ] Allow simple toplevel aliases
* [ done ] toplevel aliases with arguments
* [ fix ] weird nonsensical test case
* [ fix ] golden test files
2021-10-13 21:55:23 +01:00
André Videla
274954998b
Implement generic interpolation (#1967)
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-10-13 17:26:54 +01:00
Zoe Stafford
5c41c81883
Optimise away case statements on unit-y types (#1844) 2021-10-13 15:46:02 +01:00
Edwin Brady
dd95a549d5
Fix performance regression #1991 (#1995)
* Normalise types fully at the REPL

It was a bit odd that we only normalised the scope of function types and
not the arguments, and I can't remember the reason for that if there
even was one.

* Better way of using nf_metavars_threshold

If a term is getting big and probably needs normalising, we now have a
sizeLimit flag in quote, so we can use that instead of checking the size
afterwards. This is a handy heuristic for speeding up unification when
there's a term with lots of suspended computation. Fixes #1991
2021-10-11 23:53:52 +01:00
Alissa Tung
e15c78ce9e
[ fix #1970 ] error on mod self ref (#1977) 2021-10-08 10:09:17 +01:00
Guillaume ALLAIS
384c8874c2 [ fix #1979 ] use virtualised locs rather than EmptyFCs
For error reporting purposes it's better to have an (approximate)
virtual location for code that was introduced by the elaborator
than to have an `EmptyFC` that does not help.
2021-10-07 16:07:03 +01:00
Mathew Polzin
fa06e9936b
Warn about unreachable default clauses (#1942)
* so much experimentation

* tests that show preliminary evidence the new stuff is working.

* small amount of cleanup

* more cleanup of various troubleshooting code.

* new test case added.

* only log unreachable indices if there are any.

* when traversing deeper simply skip over defaults since they have already been reviewed.

* Remove fallback clause that the changes in this PR correctly identified as unreachable.

* tidying up more.

* move some common functions to a new Core.Case.Util module.

* refer to case builder and case tree under new parent module.

* update imports to look for CaseTree in new submodule.

* update api ipkg

* remove unneeded application operators.

* remove or comment out unreachable default clauses caught by the changes in this PR.

* a bit of code documentation and renaming for clarity.

* bump previous version in CI.

* fix API usage of Util module.

* Add issue 1079 test cases.

* forgot to add new test cases file.

* remove commented-out lines by request of RefC author.

* Use a SortedSet instead of nubbing a list.

* update new case tree import.

* Update src/Core/Case/Util.idr

Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>

* remove function with nothing to offer above and beyond a differently named copy of the same code.

* replace a large tuple with a record; discover not all of the tuple's fields were needed.

* fix shadowing warning.

Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
2021-10-02 12:55:21 +01:00
Edwin Brady
a9ccf4db4f
Experimental Scheme based evaluator (#1956)
This is for compiled evaluation at compile-time, for full normalisation. You can try it by setting the evaluation mode to scheme (that is, :set eval scheme at the REPL). It's certainly an order of magnitude faster than the standard evaluator, based on my playing around with it, although still quite a bit slower than compilation for various reasons, including:

* It has to evaluate under binders, and therefore deal with blocked symbols
* It has to maintain enough information to be able to read back a Term from the evaluated scheme object, which means retaining things like types and other metadata
* We can't do a lot of the optimisations we'd do for runtime evaluation particularly setting things up so we don't need to do arity checking

Also added a new option evaltiming (set with :set evaltiming) to display how long evaluation itself takes, which is handy for checking performance.

I also don't think we should aim to replace the standard evaluator, in general, at least not for a while, because that will involve rewriting a lot of things and working out how to make it work as Call By Name (which is clearly possible, but fiddly).

Still, it's going to be interesting to experiment with it! I think it will be a good idea to use it for elaborator reflection and type providers when we eventually get around to implementing them.

Original commit details:

* Add ability to evaluate open terms via Scheme

Still lots of polish and more formal testing to do here before we can
use it in practice, but you can still use ':scheme <term>' at the REPL
to evaluate an expression by compiling to scheme then reading back the
result.

Also added 'evaltiming' option at the REPL, which, when set, displays
how long normalisaton takes (doesn't count resugaring, just the
normalisation step).

* Add scheme evaluation mode

Different when evaluating everything, vs only evaluating visible things.
We want the latter when type checking, the former at the REPL.

* Bring support.rkt up to date

A couple of missing things required for interfacing with scheme objects

* More Scheme readback machinery

We need these things in the next version so that the next-but-one
version can have a scheme evaluator!

* Add top level interface to scheme based normaliser

Also check it's available - currently chez only - and revert to the
default slow normaliser if it's not.

* Bring Context up to date with changes in main

* Now need Idris 0.5.0 to build

* Add SNF type for scheme values

This will allow us to incrementally evaluate under lambdas, which will
be useful for elaborator reflection and type providers.

* Add Quote for scheme evaluator

So, we can now get a weak head normal form, and evaluate the scope of
a binder when we have an argument to plug in, or just quote back the
whole thing.

* Add new 'scheme' evaluator mode at the REPL

Replacing the temporary 'TmpScheme', this is a better way to try out the
scheme based evaluator

* Fix name generation for new UN format

* Add scheme evaluator support to Racket

* Add another scheme eval test

With metavariables this time

* evaltiming now times execution too

This was handy for finding out the difference between the scheme based
evaluator and compilation. Compilation was something like 20 times
faster in my little test, so that'd be about 4-500 times faster than the
standard evaluator. Ouch!

* Fix whitespace errors

* Error handling when trying to evaluate Scheme
2021-09-24 20:38:55 +01:00
madman-bob
119d8321d4
[ fix ] Use qualified type name for record elaboration (#1871) (#1948)
* [ fix ] Use qualified type name for record elaboration (#1871)

* Clarify record elaboration `Name` arguments
2021-09-24 11:23:46 +01:00
Guillaume ALLAIS
f4bd911f13 [ fix #1943 ] Allow operator names in named argument applications 2021-09-23 11:41:25 +01:00
Guillaume ALLAIS
87c1cb697f [ repl ] better printing of holes
* Fixed printing in the IDEMode (& include highlighting)
* Now also print the type of the holes
2021-09-19 17:49:51 +01:00
Edwin Brady
2e98dd6dab
Abandon auto search on undefined name (#1938)
* Abandon auto search on undefined name

These might arise from names in other modules that haven't been
imported. But it's going to be an error whatever, so give up straight
away. Fixes #1925

* Fix typo

* Fix test source

* Record possible cause when we can't solve a goal

Normally, it's just because we searched and failed. But maybe sometimes,
it's because there's an undefined name, in which case, we can include
this in the error message.

This is good to record because it means we don't abandon elaboration at
the wrong time! Say, if a search fails due to an undefined name, but it
was only in one branch of an ambiguous elaboration.

* Add necessary arguments for perf009 test
2021-09-19 14:31:29 +01:00
James Cook
971afa9f5d
Add a transform rule making (++) for List tail-recursive. (#1888) 2021-09-16 15:35:29 +01:00
stefan-hoeck
281ae86ece [ fix ] string casts on js backends 2021-09-10 08:48:29 +01:00
Guillaume ALLAIS
1f85265193 [ re #1632 ] (->) does not unify with any of TCon/Type/PrimVal 2021-09-09 18:37:49 +01:00
Stefan Höck
af5657d23a
[ performance ] Memoise toplevel constants (#1899)
* [ performance ] memoize toplevel constants

* [ test ] memoization tests

* [ fix ] fix blodwen-lazy for racket and gambit
2021-09-08 16:46:19 +01:00
Guillaume ALLAIS
b231ef0da5 [ fix #1831 ] Be more careful about checking primitive names 2021-09-07 11:23:26 +01:00
Edwin Brady
c861845757
Abandon ambiguity resolution on undefined name (#1907)
* Abandon ambiguity resolution on undefined name

This has finally annoyed me enough to do something about it. If we get a
"no such variable" error there's no point exploring other branches.

* Removes spaces from test file

One day I'll update the linter to ignore test files. We should really
accept literally anything as a possiblity for test files, even if
removing the spaces is tidier.

* Reset context before throwing in 'successful'

Although I don't think this is strictly necessary for a fatal error, we
should still for the sake of tidiness reset the state when backtracking.
2021-09-07 00:41:08 +01:00
Edwin Brady
9865765d1d
Normalise errors on display, not when they arise (#1906)
* Move Context into its own file

Just the core definition - this is so that we have access to it in
Core.Core, for inclusion in error messages, to save normalisation of
terms in errors until we actually show them.

* Normalise errors on display, not when they arise

This can save a lot of time in ambiguity resolution if the errors are
complicated, because the errors might never be displayed if it's in an
abandoned branch.

This involves lifting 'Context' out of Core.Context, because we need to
store it in Error, which is needed by Core, which in turn is needed in
Core.Context.

Also moved a couple of test caes from ttimp to idris2, so that the
errors get rendered properly and won't need updating unnecessarily. In
fact all of the ttimp tests - which were just part of the initial
scaffolding - are probably now subsumed by the idris2 tests.

* Add new coverage001 test files
2021-09-06 23:37:59 +01:00
Edwin Brady
2a5739c27a
Check primitives (fromInteger etc) reduce on LHS (#1903)
If they don't, we can't turn them into patterns to match on, and we end
up looping. Possibly we could throw a different and maybe more
informative error instead of just making an unmatchable pattern.
Fixes #1895
2021-09-05 12:37:59 +01:00
Guillaume ALLAIS
257783275e [ new ] --total cli flag 2021-09-03 12:07:29 +01:00
Guillaume ALLAIS
a7d73d0d3d [ new ] ellipses for with patterns
Rather than Agda's `...` we use the common symbol for "I don't care": `_`.
2021-08-31 22:50:46 +01:00
Guillaume ALLAIS
d289ed653d [ fix #1887 ] Parse _ <- as DoBind instead of DoBinPat 2021-08-31 22:50:22 +01:00
Stefan Höck
2465418610
[ fix ] fix #1839 (#1857)
* [ fix ] fix #1839

* [ test ] console width 0 in test
2021-08-24 15:43:22 +01:00
Guillaume ALLAIS
4a9f00078a [ close #1313 ] test case
This was fixed by, I believe, the addition of `withExtendedNS` in #1342
2021-08-20 16:47:59 +01:00
G. Allais
8d8a135237
[ fix #1496, fix #1345 ] propagate lex & lit fails too (#1850) 2021-08-20 16:47:47 +01:00
G. Allais
21c6f4fb79
[ breaking ] remove parsing of dangling binders (#1711)
* [ breaking ] remove parsing of dangling binders

It used to be the case that

```
ID : Type -> Type
ID a = a

test : ID (a : Type) -> a -> a
test = \ a, x => x
```

and

```
head : List $ a -> Maybe a
head [] = Nothing
head (x :: _) = Just x
```

were accepted but these are now rejected because:

* `ID (a : Type) -> a -> a` is parsed as `(ID (a : Type)) -> a -> a`
* `List $ a -> Maybe a` is parsed as `List (a -> Maybe a)`

Similarly if you want to use a lambda / rewrite / let expression as
part of the last argument of an application, the use of `$` or parens
is now mandatory.

This should hopefully allow us to make progress on #1703
2021-08-10 19:24:32 +01:00
Ellis Kesterton
0d6049cbcf
Fix error message for incorrect function patterns (#1816) 2021-08-09 10:00:34 +01:00
Zoe Stafford
8e1ca0eddf
Add break in each case alt in js backend (#1796)
* Add `break` in each case alt in js backend
Fixes #1795

* Remove some uneeded `break`s

* linter

* Follow @stefan-hoeck 's advice
This is neater
Note: I renamed breakAfterAssignment because it's too much work to type

* [ test ] Test for #1795

* cleanup: remove unneeded vcat
2021-07-30 07:16:23 +01:00
Guillaume ALLAIS
13ef8ba707 [ fix #1782 ] remove the case-specific code
I can't make sense of this code, it seems to try to convert the
case function corresponding to `let (a, b) = f n in ...` into a
different case function where `f n` and `(a, b)` have been unified.
But if `f n` is a bona fide stuck computation, there's no chance of
this happening.

Just turning this off solves the #1782 and only breaks one function
in the whole of the idris2 repo (I would have expected our current
termination oracle to be too weak to detect it as valid anyway!)
and one in frex (which, again, should not have been seen as terminating).

Also fixes #1460
2021-07-26 17:03:16 +01:00
Guillaume ALLAIS
230f42b697 [ re #1771 ] Do not use Erased to go under binders
In the `MkFix : f (Fix f) -> Fix f` example, using `Erased` for `f`
makes the type reduce to `[__] (Fix [__]) -> Fix [__]` and because
`[__] e1 ... en` computes to `[__]`, we end up with `[__] -> Fix [__]`
which does not reference `Fix` anymore.
2021-07-23 13:30:24 +01:00