idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-17 08:11:45 +03:00
Code Issues Projects Releases Wiki Activity
2,283 Commits 6 Branches 9 Tags 112 MiB
6c24b9ea7d
Commit Graph

1022 Commits

Author SHA1 Message Date
Mathew Polzin
6c24b9ea7d fix bad merge conflict resolution. 2021-07-15 17:27:35 -07:00
Mathew Polzin
ec3b868cb6 rename experimental command line flag and group with the other experimental feature. 2021-07-15 17:24:12 -07:00
Mathew Polzin
89125e96dd merge w/ upstream 2021-07-15 17:21:08 -07:00
Edwin Brady
f51aa22046 Bring #1719 up to date with latest changes 2021-07-15 22:04:49 +01:00
Edwin Brady
4079ae0e25 Merge branch 'master' of https://github.com/AliasQli/Idris2 into AliasQli-master 2021-07-15 21:44:26 +01:00
Edwin Brady
50c0116780
Merge pull request #1718 from edwinb/Russoul-unification 
Postpone when instantiating if type is unknown
 2021-07-15 21:16:00 +01:00
André Videla
e45d792283
Merge pull request #1701 from mattpolzin/alternative-errors 
Show error output from multiple alternative parsing branches.
 2021-07-15 20:06:25 +00:00
Edwin Brady
d9a56c5fd1 Merge branch 'unification' of https://github.com/Russoul/Idris2 into Russoul-unification 2021-07-15 20:24:27 +01:00
Mathew Polzin
883097e907 whitespace lint fix 2021-07-15 12:09:15 -07:00
Mathew Polzin
948a5ba9df noticed I was not _quite_ retaining existing behavior around Alt error processing so fixed that. updated tests. 2021-07-15 12:05:23 -07:00
Edwin Brady
fbb277f8e9
Merge pull request #1715 from edwinb/buzden-name-quote-single-brace 
Name quotes are suggested to use single brace instead of double
 2021-07-15 19:15:19 +01:00
Arnaud Bailly
ae0e4f4893
fix returned sexp for make-lemma command result (#570) 
the returned structure is inline with what Emacs idris-mode expects, so this fix
allows using C-c C-e on a hole and get it lifted as a toplevel definition
 2021-07-15 18:41:13 +01:00
Edwin Brady
b192be32b8 Merge branch 'name-quote-single-brace' of https://github.com/buzden/Idris2 into buzden-name-quote-single-brace 2021-07-15 17:57:41 +01:00
Mathew Polzin
8d8d3ef71e woops, missed the first let when resolving merge. thank goodness we are dealing with a static type system 2021-07-15 06:40:38 -07:00
Mathew Polzin
289f1cc954 merge w/ upstream. 2021-07-15 06:29:56 -07:00
Edwin Brady
f79ff202e7 Bring quotation fix up to date 
This is an update of PR #530 (Thanks to @mb64!)
 2021-07-15 14:29:12 +01:00
Edwin Brady
86aaed5ae1
Merge branch 'master' into fix-unquote-thing 2021-07-15 14:13:25 +01:00
Edwin Brady
15bc6a3980
Merge pull request #1708 from stepancheg/fork-io-array 
Fork Data.IOArray into the compiler
 2021-07-15 14:09:58 +01:00
Edwin Brady
35f23ac1d6
Merge pull request #1712 from edwinb/MarcelineVQ-elab-name-changes 
Add more name reflections
 2021-07-15 14:08:31 +01:00
Edwin Brady
9b0ebcd08b Merge branch 'elab-name-changes' of https://github.com/MarcelineVQ/Idris2 into MarcelineVQ-elab-name-changes 2021-07-15 13:16:47 +01:00
Guillaume ALLAIS
efcf44e8ba [ cosmetic ] use the whole range when underlining the problem 2021-07-15 07:32:43 +01:00
Mathew Polzin
221dadeb20 set default alt error count to 1 and create a config option that sets it to any number. 2021-07-14 20:23:29 -07:00
Mathew Polzin
1f21e787b1 Use commit to reduce the alternative parsing space as soon as an opening paren is encountered. 2021-07-14 17:22:40 -07:00
Stiopa Koltsov
47205049cf Fork Data.IOArray into the compiler 
To be able to modify `Data.IOArray` as proposed in #1677.

Currently `Data.IOArray` cannot be modified because compiler need
to be built with previous compiler. This PR removes compiler
dependency on `Data.IOArray`.
 2021-07-15 00:38:08 +01:00
Edwin Brady
5cb77ad675
Merge pull request #1704 from edwinb/with-params 
Fix 'with' under implicit parameters
 2021-07-14 15:56:58 +01:00
Edwin Brady
1dbc9a7143 Fix 'with' under implicit parameters 
The 'with' type and application need to treat the parameters with the
same plicity, but the application has just always treated them as
explicit since it never looked. It's easiest just to make them all
explicit, since this isn't a user visible type. Fixes #1695.
 2021-07-14 14:51:52 +01:00
Mathew Polzin
830e5dc12d Fix bug with what value was propagated from rhs of alt parse failure and add test case for '@' as value constructor. 2021-07-14 00:25:02 -07:00
Stiopa Koltsov
13a9676805 Use the same generated string in RefC backend as in other backends 2021-07-13 23:00:13 +01:00
Mathew Polzin
385a61a364 fix linting errors and use a public import of List1 instead of forcing other files to import List1 just to use Libraries.Text.Parser 2021-07-13 10:53:58 -07:00
Niklas Larsson
eb0c59c908
Enable incremental compilation on Windows. (#1694) 2021-07-13 11:29:34 +01:00
stefan-hoeck
f6b4f188e1 [ new ] support compile time evaluation of new integer primops 2021-07-13 11:28:02 +01:00
Rujia Liu
9dfad52173
[fix] refc backend broken with msys2 (#1668) 2021-07-13 11:27:36 +01:00
CodingCellist
80e7e179ad
[ fix #1652 ] Save casefnty to TTC (#1686) 2021-07-13 11:04:07 +01:00
Mathew Polzin
8e1f2cf4ce fix lack of error for @ used as identifier and display multiple alternative errors. 2021-07-12 23:11:43 -07:00
Edwin Brady
9bd32c4a3d Fix chez033 on windows 
This prints lots of warnings since incremental compilation is not
available, so turn that off when running on windows for now.
 2021-07-11 17:04:07 +01:00
Edwin Brady
c95ebd554d Disable incremental compilation on Windows 
It currently doesn't work anyway, so fall back to whole program
compilation which at least means the test doesn't get in the way.
 2021-07-11 16:20:47 +01:00
Edwin Brady
886962aa43 Need --script for incrementally compiled apps 
Otherwise it doesn't load the compiled modules and can't find the
compiled definitions!
 2021-07-10 23:55:45 +01:00
Edwin Brady
3e92863e1c
Merge pull request #1674 from edwinb/parameters 
A couple of parameters block fixes
 2021-07-10 21:18:07 +01:00
Edwin Brady
4ca8caeb13 Fix case split in parameter blocks 
We need to make sure variables are bound as PVar, in the end, otherwise
the case split machinery doesn't know how to handle them.
 2021-07-10 19:13:27 +01:00
Edwin Brady
26cdfc7830 Make records work in parameter blocks 
This involves making 'unelab' aware of nested names so that it can
remove the parameters from names in the current block. It's a bit of a
hacky solution, but it is also the easiest one.
Ideally we'd build the getter types directly, rather than using unelab,
but that's one to save for another time.
Fixes #1482
 2021-07-10 18:12:44 +01:00
Edwin Brady
8b45ccd264 Use chez --program rather than --script 
We're running our executables as top level programs, so this gives more
scope for optimisations, doesn't use the Chez REPL, etc.
 2021-07-10 16:40:19 +01:00
Stefan Höck
599d0635e9
[ refactor ] JS backend overhaul (#1609) 2021-07-10 11:15:21 +01:00
Zoe Stafford
0ecbd517e8
[ improvement ] VMCode (#1662) 2021-07-07 17:06:59 +01:00
Stiopa Koltsov
9c63e90fd2 Write compiler version into generated files 2021-07-06 09:35:48 +01:00
Edwin Brady
6a60680af6 Don't inline holes that are user defined names 
We inline some holes when solving them if they pose no risk to breaking
sharing, since this can speed up a few things. But if the hole was
originally a user name, we might want to refer to it, and inlining it
menas we can't since it won't be saved to disk.
 2021-07-02 15:59:56 +01:00
G. Allais
b0e297658c
[ cli ] make package file optional (#1651) 2021-07-01 14:16:29 +01:00
Alissa Tung
2865a70a6e
[ base ] add List functions (#1550) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-07-01 08:00:12 +01:00
Johann Rudloff
5e70a77310 [ docs ] Ignore empty record field docstrings 2021-06-30 22:01:26 +01:00
Johann Rudloff
7c1ab56ca0 [ docs ] Add record field docstrings to the RF-name as well 
A record field can add two names to the context, a UN-name and an
RF-name.  The docstring is now saved for both names, so that it can
always be found when one of the names can be resolved.

Previously the docstring was only saved for the UN-name which led to the
docs missing when looking up the (.fieldName) version, e.g. when listing
docs for the record type.
 2021-06-30 22:01:26 +01:00
Johann Rudloff
af9f72466f [ docs ] Fix record fields wrapped in parentheses in HTML doc 
The (implicitly added) "."-prefix when calling `isOpName` with an RF-name
leads to `isOpName` always returning true (which is correct in most
cases, where the RF is displayed as such). In case of the docs however,
we only show the name root and thus should check the "real" name of the
field (without the added dot in the beginning).
 2021-06-30 22:01:26 +01:00