Changes:
- Eff has become EffM, parameterised over (m : Type -> Type), which will
allow us to introduce new effects later, though not currently used
- Eff itself is now a collection of type synonyms which build an EffM.
It can take either one list of effects, a list of input and output
effects, or a list of effects and a function to compute output
effects; disambiguated by context
- EffT is as Eff, but takes the underlying 'm'
- Added 'sig' function for giving effect signatures.
All of the above mean we no longer need the {} syntactic sugar, though
it's still there. Old effect programs (should!) work with no or minimal
changes.
This compiles the expression and evaluates it. It will either print the
expression (if its type is an instance of Show) or run it (if its type
is IO ()), or give an error otherwise.
This causes Idris to not emit messages about "Type checking ...." while
in quiet mode, which improves the portability of tests to Windows (due
to the slash facing the other way there). It also makes tests a bit more
robust with regards to their source files changing names.
This allows extra hints, as well as constructors, to guide proof search
for auto implicit arguments.
Added test proof010 which shows how this works to simulate type classes
with overlapping instances (and consequently no injectivity restriction
or assumption)
%hint only works on functions which return an instance of a data type.
Proof search exhaustively searches hints and constructors, so use with
care especially when adding lots of recursive or overlapping hints.
Primitives for head/tail/index/cons/reverse/length now all assume the
char* is UTF8 encoded. Also updated generation of literals to encode as
UTF8. Primitives are probably not as efficient as they could be (though
some of the will be used rarely)
ASCII strings will work exactly as before.
Everything I know about UTF8 encoding has been learned in the past few
hours. Therefore, this is unlikely to be the best way to do this. Please
educate me, ideally in the form of annotated Pull Requests :).
We weren't shadowing names correctly when a class was parameterised on a
single variable and one of the methods bound the same name. This almost
never happens, but leads to very odd error messages when it does.
Fixes#2026
This means we get better error messages if there are scoping issues,
particularly as caused by 'where' clauses with missing types that can't
be inferred.
Fixes#1978
Need to expand implicits for methods in the dictionary declarataion, but
not quite the same way as for the top level function of the same name
(i.e. need to leave out the dictionary itself).
Fixes#1975
Also fix resolution rules so that determining parameters, in *all cases*
except Num instances (for defaulting to Integer), must not be
metavariables.
Syntax is:
class Foo a b c | a, b
the optional | a, b lists the determining parameters. When resolving
Foo, a and b must not be metavariables. c can be a metavariable (and
hence solved by type class resolution).
The overlapping instance check now only looks at determining parameters,
so, for example, for Foo the following instances would be considered
overlapping:
instance Foo Int Nat Bool
instance Foo Int Nat String
It now offers different errors when it couldn't prove the lemma due to
having a variable for the Integer, or when it couldn't prove it due to
having concrete values that are directly incorrect.
The changes are as follows:
+ `print` is for putting showable things to STDOUT.
+ `printLn` is for putting showable things to STDOUT with a new line
+ `putCharLn` for putting a single character to STDOUT, with a new line.
Effects has been updated accordingly.
This works only if the elaborator is in a context where it is expecting
a unique type (or a Type*) rather than a normal type. This is
EXPERIMENTAL but should(!) not cause any issues in code which uses no
unique types or Type*
This commit introduces:
* A new tactic "claim N TY" that introduces a new hole named N with
type TY
* A new tactic "unfocus" that moves the current hole to the bottom of
the hole stack
In the process of this and some other work, I also added comments and
docs to more of the core.
If after an application there are more implicit arguments expected, add
those arguments then re-elaborate the application - we often don't know
what these arguments will be until after elaborating the application
because the application itself may compute a type.
Fixes#1899
This means we can make primitives for reading/writing file handles which
are given the world state, so can be written more safely. Also, a
minimal back end can implement these rather than implementing an entire
FFI.
Updated primitive LReadStr (which can now reasonably be total, like any
foreign function, because it has a world state) and added primitive
LWriteStr.
More documentation to follow, but in brief:
- IO is now a synonym of IO' FFI_C
- IO' is parameterised over an ffi description, which explains which
types are allowed in foreign calls, and what a foreign call target is
(in C, that's a String giving the function name, for example)
- New function "foreign" for building a foreign call, given an ffi
description, call target, and the type of the call. The type is enough
to build a structure which the compiler uses to generate the call.
The type of main now needs to be IO' x (), where x can be any FFI
description.
There is currently only an ffi description for C; Javascript will
follow. FFI_C should also work for the llvm backend (it's really about
the calling convention, not the backend specifically). Small changes
will be needed to the various code generators.
Limitation: the type class constraint must be under a scoped implicit
(this is purely for parsing reasons, although I also can't immediately
think of a reason you'd want this except under an implicit...)
The syntax is the same as for other documentation, right before the
"module" declaration. For an example, see the "idrisdoc009" test. Terms
in module documentation are elaborated in a context including all of its
imports and definitions, so the documentation can provide examples and
descriptions.
The :doc command now also shows documentation for modules.
Like so:
foo : (c : Show a) => List a -> String
This means that type classes can be used as indices/parameteres of data
types (e.g. to ensure a dictionary is unchanging across a structure).
Fixes#646
They can be imported from the modules Data.Fin, Data.Vect, and Data.So
respectively.
The general thinking here is that not every program is going to need
these, and they are often used especially by newcomers in place of
something more appropriate. Also, all of them are useful for teaching,
which means it is instructive for tutorials to introduce them and have
people implement them themselves.
Add reflection-based error message improvements for Fin literals. Now,
instead of a collection of internal implementation details, a friendly
and descriptive message is returned.
See test/error005 for a demo.
Only allow matching on polymorphic arguments if they have been refined
to something concrete due to some other argument by the time they're
elaborated.
Any term which is not matchable, i.e. a function application or a
repeated variable on the left hand side, is automatically put in a
PHidden. The effect of elaborating PHidden t is to:
1. Delay the elaboration of 't' to the end of elaboration
2. When elaborating t, ensure that its value is already known due to
solving some other unification problem.
If something is PHidden, but not solvable by unification, elaboration
fails.
This finally fixes#323, and probably several other things.
Except under quasiquotation. This is to prevent any arguments being
specialised to a more specific type than the function type suggests (one
place where typecase can arise).
By popular request. Fixes#1706.
It's not the most efficient desugaring, merely translating the @s on the
left to lets on the right, so the case tree builder won't be aware of
it. Still, it provides the notation and it works nicely with showing
what is in scope and what is available in the prover and so on.
Fixes#111
Previously, if a module B imports a module A, then a module C imports B,
the public names in A would also be visible to C (i.e. B would
automatically reexport everything from A). This seems to be a bad
default.
This patch changes the default behaviour so that the only names exported
from a module are those defined in that module. If B imports A and wants
to reexport everything in A, then A should be imported with the "public"
modifier (i.e. "import public A").
Several changes have been made to the prelude, since several prelude
modules were taking advantage of the old broken behaviour.
This may cause lots of things to break. Sorry. The fix is typically just
to import the module you should have imported anyway :).
The tactic sourceLocation fills the hole with the current location in
the file. If such information is unavailable, it fails.
This is to be used by DSL implementers to provide useful error
messages that can't be caught at type-check time. Additionally, it may
prove useful for debugging and assertion libraries, so they can report
errors.
Because the tactic merely fills out an implicit argument in a particular
way, it doesn't break referential transparency, at least not of the core
language. This is similar to the technique used in Scala Virtualized.
Now, code blocks that are declared to be Idris code (with the Markdown
language specifier) are type checked, and any type checker or parser
errors that occur are retained and displayed to IDEs.
Doing so breaks typechecking, leading to nothing working any more...
passing them to lifted 'where' definitions counts as a use in the
typechecker, so *any* where clause will fail to typecheck.
This is an effect of how 'where' clauses are elaborated, and is probably
not the best behaviour (though it is better than the default which rules
our where clauses completely) so we should revisit it later if
uniqueness typing turns out to work effectively.
We need to know the kind for properly checking uniqueness under partial
application. Also, we need to propagate uniqueness right into the scope
of a binding - once we're in a unique context, any function we make has
to run in unique context or we might accidentally duplicate things.
This allows unique values to be inspected, but not updated or
destroyed. A 'Borrowed' value can be pattern matched, but cannot be used
on the right hand side, nor can any Unique values contained in the
pattern.
There is apparently a bug which causes it to segfault - I don't know if
this is an llvm bug or an idris llvm code generator bug, but I don't
want this to get in the way of further uniqueness type development.
Precision varies, and since the test is meant to check the primitives
are implementing what they're supposed to, truncation is okay. This
stops the test failing on 64 bit machines.
Proof state now contains the term in focus, its environment, and a path
through the complete term to reach that sub-term. As a result, large
proof terms are now checked more quickly
Cleaned up a couple of other things on the way...
"skip" does nothing, while "fail" produces an error. They have
corresponding reflected versions Skip and Fail. Fail has access to the
pretty printer by taking a List ErrorReportPart as its argument.
This just renames the internal name to something distinguishable. It's
still not completely clear (since it's a renaming from the user's name)
but given that the message means a user has picked the same name twice,
there's not too much else we can do easily... Certainly it's better than
"Can't unify f x with f x"...
Fixes#705
Now uses the elaborator to generate any necessary extra bindings, using
the same machinery as pattern match elaboration. The end result is that
you no longer need 'using' in a lot of cases (it is still useful if you
want to give explicit types, of course). e.g. this now works as it
stands:
data Elem : a -> Vect n a -> Type where
Here : Elem x (x :: xs)
There : Elem x xs -> Elem x (y :: xs)
isElem : DecEq a => (x : a) -> (xs : _) -> Maybe (Elem x xs)
This should also reduce the number of weird "no such variable" errors
signfificantly. In particular, it fixes#1354
A quasiquote expression can be given a goal type for the elaborator,
which helps with disambiguation. For instance, `(() : ()) quotes the
unit constructor, while `(() : Type) quotes the unit type. Both goal
types and quasiquote are typechecked in the global environment.
We mustn't inspect the laziness type, because we'll never have it. (This
is a bit of a hack and relies on never having two different types of
laziness in the same argument, but since that doesn't make sense anyway,
I believe this is safe!)
Fixes#1295
This is not backwards compatible, but as far as I know, there are no
users of postulate providers who are not me.
The old system allowed both the definition of the provider and the use
site to be involved in the determination of what is a postulate and what
is not. This is not good - users should always be in full control of
this.
The new implementation has two syntaxes:
%provide (x : t) with p
%provide postulate x with p
The first is the type provider syntax we know and love. The second
requires that the provider in fact return a type, which is then made
into the type of the resulting postulate.
Two reasons:
1. The most important: it makes error messages *so much better* :).
Because "effect'" rarely properly fails due to having a very generic
type, so any error arises later and breaks the real error which came
from lift'
2. It is much easier to explain what's going on when documenting
effects!
Apologies for breaking effectful code: I now think it is much better
this way though.
In interactive mode only (it is important that proofs can fail
temporarily during elaboration since futher information may help refine
the goal).
Fixes#1243
continued the work on getting the parser to work
works now, still work to do though
done with the parser, removed reduntant code, added metavars
maybe fixes build error...
changed test that used --exec without arg, and added warnreach which i forgot
removed out-commented code, added last metavar
Don't put explicit arguments in the top level methods (i.e. make them
point free). This means that they will be more inclined to reduce, which
helps in particular with totality checking, but possibly also with
theorem proving.
Changes
Prelude.Applicative.<$> : Applicative f => (f (a -> b)) -> (f a) -> f b
into
Prelude.Applicative.<$> : Applicative f => f (a -> b) -> f a -> f b
