Commit Graph

80 Commits

Author SHA1 Message Date
Edwin Brady
4834f2f78c Update test output
Clash in a reflection test due to conflicting merges. I'd like to find a
way to make the internally generated numbers not matter here (and
elsewhere) but I don't see an obvious way.
2020-06-08 10:39:58 +01:00
Edwin Brady
e033609310
Merge pull request #207 from mb64/assert_smaller-linear
Make assert_smaller and assert_total linear
2020-06-08 10:19:33 +01:00
Edwin Brady
d47d495744 Free standing case blocks return ()
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!
2020-06-07 22:49:19 +01:00
Edwin Brady
93022af74e More explicitness in evaluator return type
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
2020-06-06 22:20:25 +01:00
Edwin Brady
252e07833b Fix case trees at multiplicity zero
Can't ignore a constructor a multiplicity zero if the whole function is
multiplicity zero
2020-06-06 20:45:20 +01:00
Edwin Brady
c17d4ff0a5 Look inside case blocks in conversion check
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?
2020-06-04 18:21:44 +01:00
Edwin Brady
946e1b3a51 Slightly neater reflection008 test 2020-06-03 09:25:09 +01:00
Edwin Brady
3a7aedf0f4 Add reflection under (explicit) binders
This allows writing a staged well typed interpreter, for example (see
reflection008 test)
2020-06-03 09:17:37 +01:00
Edwin Brady
c682ded9c4 Reduce amount of normalisation in elab scripts
We don't want to unfold definitions in 'pure' or 'check' or 'bind' since
we want the exact expression that the script author has used.
2020-06-03 00:22:03 +01:00
Edwin Brady
d8d13d912e Add alternative example to reflection002
A bit more typesafe...
2020-06-02 23:56:30 +01:00
Edwin Brady
08b56e9e75 Add quote operation to Elab
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.
2020-06-02 23:36:20 +01:00
Edwin Brady
2a75731916 In reflection, check now takes a concrete type
So the type of Elab now gives the expected type that's being elaborated
to, meaning that we can run 'check' in the middle of scripts and use the
result.
2020-06-02 22:41:37 +01:00
Edwin Brady
9fab367f0f Reflect differently on LHS
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 ~().
2020-06-02 19:21:46 +01:00
Edwin Brady
c3ee2a3fac Change genSym behaviour
Instead of merely generating a locally unique name, use the existing
code for generating a new unique variable name in the unifier, which is
therefore globally unique.
2020-06-02 12:13:38 +01:00
Mark Barbone
c4cdebb578
Fix tests 2020-06-01 19:13:46 -04:00
Edwin Brady
1c18fe589b Forgot to add the new test again, didn't I... 2020-06-01 19:13:46 +01:00
Edwin Brady
3d2765e930 Add top level %runElab
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.
2020-06-01 19:06:10 +01:00
Edwin Brady
d5b5af91d1 Implement %macro flag
A %macro must always be fully applied. Whenever the elaborator
encounters a %macro application (except in a function LHS) it evaluates
the application and sends the result to %runElab. So:

%macro
foo : args -> Elab TT
...
def = foo a b c

is equivalent to

foo : args -> Elab TT
...
def = %runElab foo a b c
2020-06-01 17:55:54 +01:00
Edwin Brady
d45f92fd97 Add some reflected name manipulation
genSym, for generating a unique global name, and inCurrentNS for putting
a name in the current namespace.
2020-06-01 15:13:42 +01:00
Edwin Brady
02d371a94b Add reflection operation for adding declarations
Declarations can be quoted with `[ decl ]. See reflection004 for an
example.
2020-06-01 15:01:52 +01:00
Edwin Brady
e6f6c105d1 Reflection primitives for querying names/types
See reflection003 test for some examples
2020-06-01 14:26:37 +01:00
Edwin Brady
e2aabd6602 Add syntax for quoting names
`{{ n }} gives a value of type Name. No name resolution is attempted (so
no namespaces added etc)
2020-06-01 13:39:18 +01:00
Edwin Brady
2eb2ce6097 Add Bits primitives
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'.
2020-06-01 11:48:03 +01:00
Edwin Brady
106235c165 Allow scripts to inspect goal
If available (sometimes, say a top level expression, it might need
inferring so there'll be no goal available). Also add the ability to log
the current goal, or indeed any term.
2020-05-31 14:33:34 +01:00
Edwin Brady
85c002c771 Progress on elaborator reflection
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)
2020-05-31 01:36:54 +01:00
Edwin Brady
26e6e1ed82 Calculate compile time references even in case
If we don't do this, we don't look inside case blocks to check they
cover, and so we might miss coverage errors in nested case blocks.
Fixes #202
2020-05-30 21:53:29 +01:00
Edwin Brady
ecaa73bad5 Update test result
Not sure why this didn't fail for me locally... possibly libraries out
of sync.
2020-05-30 17:30:31 +01:00
Edwin Brady
3f914889b8 Add visibility rules on types
Can't export a type which refers to a private name. This has caught a
couple of visibility errors in the libraries, code and tests, so they've
been updated too.
2020-05-30 17:03:15 +01:00
Edwin Brady
e1dbcad2fc Make a start on reflection
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.
2020-05-29 22:40:29 +01:00
Edwin Brady
d869eb666c Experiment %syntactic flag on with
This means it abstracts over the value syntactically, rather than by
value, and can significantly speed up elaboration where large types are
involved, at a cost of being less general. Try it if "with" is slow.

There are more flags we want on with (well, at least one: "proof")
2020-05-29 16:39:11 +01:00
Edwin Brady
aad56c723f
Merge pull request #191 from edwinb/totality
Totality checking
2020-05-28 16:28:06 +01:00
Edwin Brady
8c5d5055fa Update scheme
Changing the prelude totality default means we need to update the scheme
to be able to cope with its new meaning
2020-05-28 16:05:08 +01:00
Tim Süberkrüb
42a1522a3b Try to make Windows happy with backslashes 2020-05-28 16:42:56 +02:00
Edwin Brady
2223d50c3a Skip totality check on case blocks and MNs
These are checked as part of checking the top level names
2020-05-28 15:32:46 +01:00
Tim Süberkrüb
c2dfe7de7f Add popen and pclose from Idris 1 2020-05-28 12:58:03 +02:00
Niklas Larsson
696db7f58f
Merge pull request #169 from andylokandy/pathcom
Use Path in the compiler
2020-05-27 21:23:29 +02:00
Edwin Brady
c88bf7af8d Fix import loading
This was taking too long, and adding too many things, because it was
going too deep in the name of having everything accessible at the REPL
and for the compiler. So, it's done a bit differently now, only chasing
everything on a "full" load (i.e., final load at the REPL)

This has some effects:
+ As systems get bigger, load time gets better (on my machine, checking
  Idris.Main now takes 52s from scratch, down from 76s)
+ You might find import errors that you didn't previously get, because
  things were being imported that shouldn't have been. The new way is
  correct!

An unfortunate effect is that sometimes you end up getting "undefined
name" errors even if you didn't explicitly use the name, because
sometimes a module uses a name from another module in a type, which then
gets exported, and eventually needs to be reduced. This mostly happens
because there is a compile time check that should be done which I
haven't implemented yet. That is, public export definitions should only
be allowed to use names that are also public export. I'll get to this
soon.
2020-05-27 15:49:03 +01:00
Jan de Muijnck-Hughes
8b062f47cc Allow cli given option overriding for ipkg cmds.
As it was in Idris1 being able to override some, or introduce new, options to an Idris IPKG is beneficial. For example, generate code for multiple codegens from a single source.

Overridable options are:

+ `--quiet`
+ `--verbose`
+ `--timing`
+ `--dumpcases <file>`
+ `--dumplifted <file>`
+ `--dumpvmcode <file>`
+ `--debug-elab-check`
2020-05-26 14:41:09 +01:00
Jan de Muijnck-Hughes
54fd78a956 Fixed fragility of ipkg file parsing.
+ Explicitly check if an IPKG has the correct suffix.
+ Add missing case that could return a malformed error message.
2020-05-26 14:41:09 +01:00
Jan de Muijnck-Hughes
68a4ad2e1c New test for detecting overridable options for IPKG commands. 2020-05-26 14:41:09 +01:00
andylokandy
712a4df140 Gather the straw isWindowss 2020-05-26 17:59:14 +08:00
Jinwoo Lee
4a52a84113 update golden files 2020-05-25 10:06:52 -07:00
Edwin Brady
81e9214c6f Fix build
Showing a hole should show normalised types for the locals
2020-05-25 16:45:33 +01:00
Edwin Brady
bbd3986cfc
Merge pull request #153 from ohad/ide-protocol-holes
Ide protocol holes
2020-05-25 15:43:52 +01:00
Edwin Brady
3120fcb84a Allow _ for names in pi binders
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.
2020-05-25 13:14:51 +01:00
Ohad Kammar
f4797be529 Merge branch 'master' of github.com:idris-lang/Idris2 into ide-protocol-holes 2020-05-25 11:51:39 +01:00
Ohad Kammar
92eaa247a6 Refactor FoundHoles : REPLResult to carry more structured information about holes 2020-05-25 10:38:22 +01:00
Edwin Brady
227bd3b457
Merge pull request #119 from idris-lang/idemode
[ refactor ] Idris.IDEMode.CaseSplit
2020-05-25 09:09:37 +01:00
Edwin Brady
9970c66417 Warn on detecting unreachable patterns
I don't know how complete this is, but it certainly detects some of the
most obvious cases which are most likely to be bugs.

While I'm at it, this is as good a time as any to add a general way of
reporting warnings, similar to the way of reporting errors.
2020-05-25 00:16:49 +01:00
Edwin Brady
498421a236 All functions now need to be covering by default
This has caught a couple of things in the Idris 2 code base itself. Some
tests needed partial annotations too.
2020-05-24 19:58:20 +01:00