Commit Graph

201 Commits

Author SHA1 Message Date
G. Allais
4a61146ba0
[ fix #705 ] Normalise primitives in mkPat (#718)
[ log ] prettier log for pats & clauses
[ re #650 ] Even lazier
[ fix #705 ] normalise primitives in mkPat
[ refactor ] introduce getPrimitiveNames
2020-10-02 12:22:57 +01:00
russoul
a667aae797 Fix another DPair parsing regression 2020-10-02 11:22:48 +01:00
Ruslan Feizerahmanov
1d99a28176
Add Bifunctor interface (#701) 2020-09-30 10:51:07 +01:00
G. Allais
3df1f9c476
[ fix #63 ] interleaving let binders and local declarations (#691) 2020-09-28 13:15:22 +01:00
Guillaume ALLAIS
416b9578e5 [ fix #37 ] Use filename if we already know it 2020-09-24 15:56:23 +01:00
Guillaume ALLAIS
0d08c0b81b [ log ] for desugaring of idioms 2020-09-24 15:27:40 +01:00
MarcelineVQ
961a28ee64 fix idiom brackets to account for IAlternative
Things like (,) () aren't straightforward IVar's but are IAlternative's
which present options about how the term should resolve. [| |] was not
accounting for this.
2020-09-24 15:27:40 +01:00
Guillaume ALLAIS
cc31076849 [ test ] more corner cases
Making sure the test can distinguish between truncating & rounding.
2020-09-23 19:48:58 +01:00
Guillaume ALLAIS
621a9202ed [ test ] making sure cast works 2020-09-23 19:48:58 +01:00
Christian Rasmussen
091465525b Remove FArgList 2020-09-23 18:33:19 +01:00
G. Allais
8d09ec9c93
[ new ] comma-separated interface parameters (#682) 2020-09-19 15:29:23 +01:00
G. Allais
3008c48f77
Adding a whole bunch of tuple sections (#680) 2020-09-19 14:51:57 +01:00
Guillaume ALLAIS
2bb95e59ef [ re #660 ] eta-contract parameter candidates 2020-09-16 15:45:16 +01:00
Guillaume ALLAIS
1152aa3cdd [ re #660 ] inline lets when detecting parameters 2020-09-16 15:45:16 +01:00
Giuseppe Lomurno
98e54cea2f Missing runElab decl check 2020-09-16 12:06:38 +01:00
Guillaume ALLAIS
65e194e9bb [ re #660 ] Positivity checking for empty types 2020-09-14 18:37:47 +01:00
Ohad Kammar
0600a9ba11 Fix bug #654
Auxiliary functions introduced in elaboration (e.g., through case splits and with clauses) now
have the same totality annotation as the function they're defined in.

Moved auxiliary function `findSetTotal` into `Context.idr` since it's
now used by `ProcessDef.idr` too.

Added a totality requirement argument to `checkClause` so that the
with-clause case could propagate it to the functions it generates in
elaboration.

Sandwhich the rhs elaboration in pattern matches with code that sets
the global, default, totality requirement to the current one, and
restores the previous default afterwards. It's a bit of a hacky way to
do it, but I don't think we have a better alternative with the current
design.
2020-09-10 08:08:59 +01:00
G. Allais
1963ac8786
[ fix #650 ] Lazier match in NPrimVal vs. ConCase (#655) 2020-09-09 17:17:07 +01:00
G. Allais
a0c0974676
[ debug ] pretty printer for case trees (#652) 2020-09-09 16:22:22 +01:00
russoul
9565f6cf8b Fix DPair parsing 2020-09-05 11:08:44 +01:00
G. Allais
937aa8fc43
[ refactor ] introducing Namespace (#638)
Until now namespaces were stored as (reversed) lists of strings.
It led to:

* confusing code where we work on the underlying representation of
  namespaces rather than say what we mean (using `isSuffixOf` to mean
  `isParentOf`)

* potentially introducing errors by not respecting the invariant cf.
  bug report #616 (but also name generation in the scheme backend
  although that did not lead to bugs as it was self-consistent AFAICT)

* ad-hoc code to circumvent overlapping interface implementation when
  showing / pretty-printing namespaces

This PR introduces a `Namespace` newtype containing a list of strings.
Nested namespaces are still stored in reverse order but the exposed
interface aims to support programming by saying what we mean
(`isParentOf`, `isApproximationOf`, `X <.> Y` computes to `X.Y`, etc.)
irrespective of the underlying representation.
2020-09-05 09:41:31 +01:00
Guillaume ALLAIS
529944267b Revert "[ refactor ] Introducing Namespace and ModuleIdent (#631)"
This reverts commit 481dc431e7.
2020-09-04 09:16:06 +01:00
G. Allais
481dc431e7
[ refactor ] Introducing Namespace and ModuleIdent (#631)
Until now namespaces were stored as (reversed) lists of strings.
It led to:

* confusing code where we work on the representation rather than say
  what we mean (e.g. using `isSuffixOf` to mean `isParentOf`)

* potentially introducing errors by not respecting the invariant cf.
  bug report #616 (but also name generation in the scheme backend
  although that did not lead to bugs as it was self-consistent AFAICT)

* ad-hoc code to circumvent overlapping interface implementations when
  showing / pretty-printing namespaces

This introduces a Namespace newtype containing non-empty lists of
strings. Nested namespaces are still stored in reverse order but the
exposed interface aims to support programming by saying what we mean
(`isParentOf`, `isApproximationOf`, `X <.> Y` computes to `X.Y`, etc.)
irrespective of the underlying representation.
2020-09-02 20:05:33 +01:00
Guillaume ALLAIS
b449e5ae8a [ fix #361 ] Use the default totality by default 2020-08-31 16:42:53 +01:00
MarcelineVQ
57e7f14bca add binary literals
Written via "0b" in the manner of other literals. e.g. 0b111001 = 57
2020-08-31 08:48:05 +01:00
russoul
7de26e7d75 Fix #616 2020-08-30 19:32:33 +01:00
Guillaume ALLAIS
9c59542081 [ new ] allow auto fields in records 2020-08-28 11:38:10 +01:00
Guillaume ALLAIS
c17c6fc522 [ log ] stuck functions found during evaluation 2020-08-27 19:42:52 +01:00
Guillaume ALLAIS
e64a3e910c [ test ] cleanup basic044
All of these internal names are making the output fragile. This
cleanup should allow us to only have to update the golden file
when there is a genuinely interesting change.
2020-08-25 09:33:39 +01:00
Alex Gryzlov
ef5299733a
refactor Data.String.Parser (#579) 2020-08-22 08:13:34 +01:00
G. Allais
56209de4ca
[ close #270 ] Add FC to Binder (#296) 2020-08-21 19:03:53 +01:00
Niklas Larsson
5f1d391242 Make the run script executable 2020-08-21 12:24:23 +02:00
Niklas Larsson
2a45854b96 Add CI checking for the API 2020-08-21 11:51:21 +02:00
G. Allais
da78ac4783
[ new ] topics for logging levels (#569) 2020-08-20 18:45:34 +01:00
karroffel
7d046652d8
add support for more casts from and to BitsN types (#548)
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2020-08-20 15:01:09 +01:00
Kamil Shakirov
1d601384ce Rename --consolewidth option to --console-width for consistency 2020-08-19 11:59:31 +01:00
Giuseppe Lomurno
63c15352f4 Prettyprinting hole context 2020-08-18 19:25:36 +01:00
Giuseppe Lomurno
cef2fbbccd Better term printing 2020-08-18 19:25:36 +01:00
Giuseppe Lomurno
42404c2d9d Automatic console width detection 2020-08-18 19:25:36 +01:00
Giuseppe Lomurno
f658ce357f More improvements
- More migrations from String to Doc
- File context in parser errors
2020-08-18 19:25:36 +01:00
Giuseppe Lomurno
607352a191 Error suggestions 2020-08-18 19:25:36 +01:00
Giuseppe Lomurno
6298a6741d Adds bounds to compiler parser
- Added primitive to compiler parser for precise text boundaries
- Reworked parser with the new primitive
2020-08-18 19:25:36 +01:00
Giuseppe Lomurno
5e9837828a Implementations and errors
- Added initial implementations for terms and values
- Error messages converted to pretty printer
- Colorization for error messages
- Color and console width option both as command line and repl command
2020-08-18 19:25:36 +01:00
Giuseppe Lomurno
df4f990b3c PTerm and error intial prettyprinting 2020-08-18 19:25:36 +01:00
Edwin Brady
04e05e3f86 Fix repeated argument check
As it was, it could break if the argument was repeated more than twice.
When checking dot patterns, we need to check that no further holes are
solved, and that the pattern variable doesn't unify with some other
pattern variable, but if it had already made progress (either for a good
or bad reason) we missed this. Fixes #536
2020-08-10 14:03:34 +01:00
Edwin Brady
15b31e69d0
Merge pull request #533 from edwinb/dpair-parse
Refactor grammar for dependent pairs
2020-08-07 17:04:39 +01:00
Edwin Brady
b786621ed6 Refactor grammar for dependent pairs
As it was, there was significant backtracking for big expressions,
getting to the end, not finding a **, so having to try again for
application expressions. Fixes #532
2020-08-07 16:30:25 +01:00
Giuseppe Lomurno
c28133b7d9 Renamed IsString to FromString
- Renaming of the string overload interface
- Added test cases for both string and integer literals overload
2020-08-05 02:33:05 +02:00
Edwin Brady
28bb45c61f
Merge pull request #522 from edwinb/more-search
More search improvements
2020-08-04 22:05:23 +01:00
Edwin Brady
45aa8f5815 Add a test for proof search 2020-08-04 20:55:48 +01:00