It's disappointing to have to do this, but I think necessary because
various issue reports have shown it to be unsound (at least as far as
inference goes) and, at the very least, confusing. This patch brings us
back to the basic rules of QTT.
On the one hand, this makes the 1 multiplicity less useful, because it
means we can't flag arguments as being used exactly once which would be
useful for optimisation purposes as well as precision in the type. On
the other hand, it removes some complexity (and a hack) from
unification, and has the advantage of being correct! Also, I still
consider the 1 multiplicity an experiment.
We can still do interesting things like protocol state tracking, which
is my primary motivation at least.
Ideally, if the 1 multiplicity is going to be more generall useful,
we'll need some kind of way of doing multiplicity polymorphism in the
future. I don't think subtyping is the way (I've pretty much always come
to regret adding some form of subtyping).
Fixes#73 (and maybe some others).
Local hints need to reduce (just like global hints do) so we expand
their definition to the lifted name before applying them.
We're identifying the global hints by knowing that the binder name is a
nested function name. This is a bit of hack, and it'd probably be better
to record that information in the binder instead, but that's a more
substantial change than I want to do right now.
This allows, for exmaple, to have apostrophes in module names.
Test was added only for chez, however this should be viable for all
targets with `:exec` implemented.
There's some missing flexibility in how foreign specifiers can be used with
scheme that is addressed here with minimal changes to how scheme specifiers
are read. This opens up uses for users that they otherwise would have had
to modify the compiler's support files to accomplish.
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.
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.
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
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
This has involved quite a bit of reorganisation and some improvements in
resugaring so that the results look nice. In summary:
* Expression search now gives back a RawImp rather than a checked term,
which allows it to include case expressions
* Case with one pattern is resugared to a destructuring let
* Some name generation issues address in function generation
We look at intermediate results for local variables which are functions
that return a concrete type, or recursive calls that return a single
constructor type. In these cases, we:
* let bind the local variable/recursive call
* generate a new definition for the scope, as a 'case' function
When we recursively generate the definition, it's a bit more restricted
so as not to explode the search space. We only take the first result, we
only look one constructor deep, and we go right to left on variable
splitting so only deconstruct the name we've just added.
These continue the search from :ps and :gd next respectively, giving the
next search result until there are no more results.
Correspondingly, added ':proof-search-next' and ':generate-def-next' in
IDE mode, which continue the search from the previous ':proof-search'
and ':generate-def' respectively.
...until the definition is complete. This is necessary since sometimes
information outside the case block can help resolve interfaces, and in
the simplest case, we might just have delayed resolving a default
Integer. It turns out this was also an obscure bug waiting to happen
with coverage checking of nested case blocks (so there's a test update
there too).
Fixes#443
In a 'Bind', normalise the result of the first action, rather than
quoting the HNF. This improves performance since the HNF could be quite
big when quoted back.
Ideally, we wouldn't have to quote and unquote here, and we can probably
achieve this by tinkering with the evaluator.
This has an unfortunate effect on the reflection002 test, in that the
"typed template Idris" example now evaluates too much. But, I think the
overall performance is too important for the primary motivation
behind elaborator reflection. I will return to this!
Instead of just the cursory name update that we used to do (which didn't
work properly anyway for a lot of reasons), now we add aliases for all
the names in the imported module.
So, like Idris 1, every global has a canonical name by which we can
refer to it, but it can also have aliases via "import ... as".
If we have a delayed thing, but we don't yet know the expected type,
don't commit to forcing because the expected type might turn out to be a
delay.
Fixes#395
'convert' doesn't solve holes, so might reject things that are solvable.
This can be an issue when resolving interfaces, because we were using
convert for arguments of the invertible holes that arise when trying to
resolve them. Fixes#66.
We need to make sure they are inferred again when elaborating methods,
so substitute in a _ in method types before substituting in the explicit
parameters.
In future, it might (probably will) also be useful to allow giving the
implicit parameters explicitly when defining implementations.
Fixes#374
We need to check below top level too, since there could be holes that
we're happy to resolve by searching. The linearity test added
illustrates a place where this is needed.
The namespace parser was not requiring a minimum indentation and instead
based its indentation on the following line, which meant that a line like:
namespace Foo
foodef : Int
placed foodef into namespace Foo instead of the module's top level.
And so made it unclear when a namespace ends.
Without --no-index, git compares the files with their state in HEAD.
But we want to compare them to each other! This explain why we were
getting no output whatsoever.
With --word-diff=color, we can easily spot the small changes anywhere in
a line.
When runing in interactive mode, the diff between expected and output is not being show,
Supposedly, Git-diff returns 0 on successful run and a non-zero for error.
However, this is not being picked up by the test suite.
We change git-diff's error reporting to be more diff like in which:
+ +ve indicates that there is a diff.
+ 0 indicates the files are the same.
+ -ve program error.
This should make diff reporting more robust.
This involves new primitives GCPtr and GCAnyPtr which are pointer types
that have finalisers attached. The finalisers are run when the
associated pointer goes out of scope.
In the test, I am assuming that the GC will only be called once, right
at the end. Otherwise, the output isn't guaranteed to be deterministic!
Let's see how this assumption holds...
This is currently Chez only. I think it'll be easy enough to add to
the Racket and Gambit back ends too.
Fixes#116. This is the solution Idris 1 took, and while it is a special
case, the syntax does make it explicit (in a way) that the result of the
case is unused - if you mean something other than (), you must now say
so!
Another one from the "stop trying to be clever" files :). Instead of a
continuation for fallthrough in the evaluator, be explicit about whether
there's a result, no match, or evaluation is stuck.
Fixes#70
This is quite fiddly as it the blocks might be in different contexts so
we need to keep track of which variables correspond in the scrutinees of
the blocks. Once that's done, check the terms at the leaves convert,
then check the corresponding variables convert.
This may not be perfect yet, because we only look at case scrutinees to
find correspondence. It might also be a bit slower than it could be, but
at least these checks are quite rare.
Fixes#208 and maybe some others?
Allows quoting a term back to a TTImp. Test reflection007 shows one
possible use for this, building a reflected, type safe, representation
of an expression.
On the LHS, we want to match against the reflected thing, so FC and
implicits need to turn into match anything patterns, or we won't match
anything at all. This means we can put quoted terms on the LHS, with
pattern variables under ~().
This invokes a script of type Elab (). %runElan in a term invokes a
script of type Elab TT. The elaborator now pushes in that type, so that
it'll report an appropriate error if you give it a script of the wrong
type.
Including appropriate casts, and Num/Eq/Ord/Show implementations.
Also includes new primitives in Data.Buffer, and calls to foreign
functions in C as 'unsigned'.
Add %runElab and start on scripts, although all they can do so far is
check a term. This does gives us, sort of, "template Idris" (as
demonstrated in test reflection002)
Don't get too excited yet - I want this in so that it doesn't get too
out of sync, but I still have to think about exactly how it's going to
work in practice.
This is mostly to make it easier to write linear function types without
having to invent names for everything, which might be noisy. Also it
improves the display of linear function types when the name isn't used
in the scope.
